nix-grpc-store-spec
checks.aarch64-linux.spec
· build #663
· 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" -> CQueued, "c2" -> CIdle),46 schedFixed::scheduler::crashes: 0,47 schedFixed::scheduler::entry: [],48 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),49 schedFixed::scheduler::mAssigned: Set(),50 schedFixed::scheduler::mBuild: Set(),51 schedFixed::scheduler::mDone: Set(),52 schedFixed::scheduler::mExpect: Set(),53 schedFixed::scheduler::mResult: Set(),54 schedFixed::scheduler::mRetry: Set(),55 schedFixed::scheduler::mRevoke: Set(),56 schedFixed::scheduler::mSchedule: Set("c1"),57 schedFixed::scheduler::published: 0,58 schedFixed::scheduler::publishedBy: Set(),59 schedFixed::scheduler::ws:60 Map(61 "w1" ->62 {63 attached: Set(),64 built: false,65 expecting: false,66 running: false,67 session: true,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: true,77 up: true78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),85 schedFixed::scheduler::crashes: 0,86 schedFixed::scheduler::entry:87 [{ followers: Set("c1"), leased: true, worker: "w1" }],88 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),89 schedFixed::scheduler::mAssigned: Set(("c1", "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" -> CQueued, "c2" -> CIdle),125 schedFixed::scheduler::crashes: 0,126 schedFixed::scheduler::entry:127 [{ followers: Set("c1"), leased: true, worker: "w1" }],128 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),129 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),130 schedFixed::scheduler::mBuild: Set(),131 schedFixed::scheduler::mDone: Set(),132 schedFixed::scheduler::mExpect: Set(),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: true,146 running: true,147 session: true,148 up: true149 },150 "w2" ->151 {152 attached: Set(),153 built: false,154 expecting: false,155 running: false,156 session: true,157 up: true158 }159 )160}161162[State 4]163{164 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),165 schedFixed::scheduler::crashes: 1,166 schedFixed::scheduler::entry:167 [{ followers: Set("c1"), leased: true, worker: "w1" }],168 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),169 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),170 schedFixed::scheduler::mBuild: Set(),171 schedFixed::scheduler::mDone: Set(),172 schedFixed::scheduler::mExpect: Set(),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: false,188 up: false189 },190 "w2" ->191 {192 attached: Set(),193 built: false,194 expecting: false,195 running: false,196 session: true,197 up: true198 }199 )200}201202[State 5]203{204 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),205 schedFixed::scheduler::crashes: 1,206 schedFixed::scheduler::entry:207 [{ followers: Set("c1"), leased: true, worker: "w1" }],208 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),209 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),210 schedFixed::scheduler::mBuild: Set(),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("c2"),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: true,237 up: true238 }239 )240}241242[State 6]243{244 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),245 schedFixed::scheduler::crashes: 1,246 schedFixed::scheduler::entry:247 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],248 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),249 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),250 schedFixed::scheduler::mBuild: Set(),251 schedFixed::scheduler::mDone: Set(),252 schedFixed::scheduler::mExpect: Set(),253 schedFixed::scheduler::mResult: Set(),254 schedFixed::scheduler::mRetry: Set(),255 schedFixed::scheduler::mRevoke: Set(),256 schedFixed::scheduler::mSchedule: Set(),257 schedFixed::scheduler::published: 0,258 schedFixed::scheduler::publishedBy: Set(),259 schedFixed::scheduler::ws:260 Map(261 "w1" ->262 {263 attached: Set(),264 built: false,265 expecting: false,266 running: false,267 session: false,268 up: false269 },270 "w2" ->271 {272 attached: Set(),273 built: false,274 expecting: false,275 running: false,276 session: true,277 up: true278 }279 )280}281282[State 7]283{284 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),285 schedFixed::scheduler::crashes: 2,286 schedFixed::scheduler::entry:287 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],288 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),289 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),290 schedFixed::scheduler::mBuild: Set(),291 schedFixed::scheduler::mDone: Set(),292 schedFixed::scheduler::mExpect: Set(),293 schedFixed::scheduler::mResult: Set(),294 schedFixed::scheduler::mRetry: Set(),295 schedFixed::scheduler::mRevoke: Set(),296 schedFixed::scheduler::mSchedule: Set(),297 schedFixed::scheduler::published: 0,298 schedFixed::scheduler::publishedBy: Set(),299 schedFixed::scheduler::ws:300 Map(301 "w1" ->302 {303 attached: Set(),304 built: false,305 expecting: false,306 running: false,307 session: false,308 up: false309 },310 "w2" ->311 {312 attached: Set(),313 built: false,314 expecting: false,315 running: false,316 session: false,317 up: false318 }319 )320}321322[State 8]323{324 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),325 schedFixed::scheduler::crashes: 2,326 schedFixed::scheduler::entry:327 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],328 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),329 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),330 schedFixed::scheduler::mBuild: Set(("c2", "w1")),331 schedFixed::scheduler::mDone: Set(),332 schedFixed::scheduler::mExpect: Set(),333 schedFixed::scheduler::mResult: Set(),334 schedFixed::scheduler::mRetry: Set(),335 schedFixed::scheduler::mRevoke: Set(),336 schedFixed::scheduler::mSchedule: Set(),337 schedFixed::scheduler::published: 0,338 schedFixed::scheduler::publishedBy: Set(),339 schedFixed::scheduler::ws:340 Map(341 "w1" ->342 {343 attached: Set(),344 built: false,345 expecting: false,346 running: false,347 session: false,348 up: false349 },350 "w2" ->351 {352 attached: Set(),353 built: false,354 expecting: false,355 running: false,356 session: false,357 up: false358 }359 )360}361362[State 9]363{364 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),365 schedFixed::scheduler::crashes: 2,366 schedFixed::scheduler::entry:367 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],368 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),369 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),370 schedFixed::scheduler::mBuild: Set(("c2", "w1")),371 schedFixed::scheduler::mDone: Set(),372 schedFixed::scheduler::mExpect: Set(),373 schedFixed::scheduler::mResult: Set(),374 schedFixed::scheduler::mRetry: Set(),375 schedFixed::scheduler::mRevoke: Set(),376 schedFixed::scheduler::mSchedule: Set(),377 schedFixed::scheduler::published: 0,378 schedFixed::scheduler::publishedBy: Set(),379 schedFixed::scheduler::ws:380 Map(381 "w1" ->382 {383 attached: Set(),384 built: false,385 expecting: false,386 running: false,387 session: false,388 up: false389 },390 "w2" ->391 {392 attached: Set(),393 built: false,394 expecting: false,395 running: false,396 session: true,397 up: true398 }399 )400}401402[State 10]403{404 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),405 schedFixed::scheduler::crashes: 2,406 schedFixed::scheduler::entry: [],407 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),408 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),409 schedFixed::scheduler::mBuild: Set(("c2", "w1")),410 schedFixed::scheduler::mDone: Set(),411 schedFixed::scheduler::mExpect: Set(),412 schedFixed::scheduler::mResult: Set(),413 schedFixed::scheduler::mRetry: Set("c1", "c2"),414 schedFixed::scheduler::mRevoke: Set(),415 schedFixed::scheduler::mSchedule: Set(),416 schedFixed::scheduler::published: 0,417 schedFixed::scheduler::publishedBy: Set(),418 schedFixed::scheduler::ws:419 Map(420 "w1" ->421 {422 attached: Set(),423 built: false,424 expecting: false,425 running: false,426 session: false,427 up: false428 },429 "w2" ->430 {431 attached: Set(),432 built: false,433 expecting: false,434 running: false,435 session: true,436 up: true437 }438 )439}440441[State 11]442{443 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),444 schedFixed::scheduler::crashes: 2,445 schedFixed::scheduler::entry: [],446 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),447 schedFixed::scheduler::mAssigned: Set(),448 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),449 schedFixed::scheduler::mDone: Set(),450 schedFixed::scheduler::mExpect: Set(),451 schedFixed::scheduler::mResult: Set(),452 schedFixed::scheduler::mRetry: Set("c1", "c2"),453 schedFixed::scheduler::mRevoke: Set(),454 schedFixed::scheduler::mSchedule: Set(),455 schedFixed::scheduler::published: 0,456 schedFixed::scheduler::publishedBy: Set(),457 schedFixed::scheduler::ws:458 Map(459 "w1" ->460 {461 attached: Set(),462 built: false,463 expecting: false,464 running: false,465 session: false,466 up: false467 },468 "w2" ->469 {470 attached: Set(),471 built: false,472 expecting: false,473 running: false,474 session: true,475 up: true476 }477 )478}479480[State 12]481{482 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),483 schedFixed::scheduler::crashes: 2,484 schedFixed::scheduler::entry: [],485 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),486 schedFixed::scheduler::mAssigned: Set(),487 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),488 schedFixed::scheduler::mDone: Set(),489 schedFixed::scheduler::mExpect: Set(),490 schedFixed::scheduler::mResult: Set(),491 schedFixed::scheduler::mRetry: Set("c2"),492 schedFixed::scheduler::mRevoke: Set(),493 schedFixed::scheduler::mSchedule: Set("c1"),494 schedFixed::scheduler::published: 0,495 schedFixed::scheduler::publishedBy: Set(),496 schedFixed::scheduler::ws:497 Map(498 "w1" ->499 {500 attached: Set(),501 built: false,502 expecting: false,503 running: false,504 session: false,505 up: false506 },507 "w2" ->508 {509 attached: Set(),510 built: false,511 expecting: false,512 running: false,513 session: true,514 up: true515 }516 )517}518519[State 13]520{521 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),522 schedFixed::scheduler::crashes: 2,523 schedFixed::scheduler::entry: [],524 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),525 schedFixed::scheduler::mAssigned: Set(),526 schedFixed::scheduler::mBuild: Set(("c2", "w1")),527 schedFixed::scheduler::mDone: Set(),528 schedFixed::scheduler::mExpect: Set(),529 schedFixed::scheduler::mResult: Set(),530 schedFixed::scheduler::mRetry: Set("c1", "c2"),531 schedFixed::scheduler::mRevoke: Set(),532 schedFixed::scheduler::mSchedule: Set("c1"),533 schedFixed::scheduler::published: 0,534 schedFixed::scheduler::publishedBy: Set(),535 schedFixed::scheduler::ws:536 Map(537 "w1" ->538 {539 attached: Set(),540 built: false,541 expecting: false,542 running: false,543 session: false,544 up: false545 },546 "w2" ->547 {548 attached: Set(),549 built: false,550 expecting: false,551 running: false,552 session: true,553 up: true554 }555 )556}557558[State 14]559{560 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),561 schedFixed::scheduler::crashes: 2,562 schedFixed::scheduler::entry: [],563 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),564 schedFixed::scheduler::mAssigned: Set(),565 schedFixed::scheduler::mBuild: Set(("c2", "w1")),566 schedFixed::scheduler::mDone: Set(),567 schedFixed::scheduler::mExpect: Set(),568 schedFixed::scheduler::mResult: Set(),569 schedFixed::scheduler::mRetry: Set("c1"),570 schedFixed::scheduler::mRevoke: Set(),571 schedFixed::scheduler::mSchedule: Set("c1", "c2"),572 schedFixed::scheduler::published: 0,573 schedFixed::scheduler::publishedBy: Set(),574 schedFixed::scheduler::ws:575 Map(576 "w1" ->577 {578 attached: Set(),579 built: false,580 expecting: false,581 running: false,582 session: false,583 up: false584 },585 "w2" ->586 {587 attached: Set(),588 built: false,589 expecting: false,590 running: false,591 session: true,592 up: true593 }594 )595}596597[State 15]598{599 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),600 schedFixed::scheduler::crashes: 2,601 schedFixed::scheduler::entry: [],602 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),603 schedFixed::scheduler::mAssigned: Set(),604 schedFixed::scheduler::mBuild: Set(("c2", "w1")),605 schedFixed::scheduler::mDone: Set(),606 schedFixed::scheduler::mExpect: Set(),607 schedFixed::scheduler::mResult: Set(),608 schedFixed::scheduler::mRetry: Set("c1"),609 schedFixed::scheduler::mRevoke: Set(),610 schedFixed::scheduler::mSchedule: Set("c1", "c2"),611 schedFixed::scheduler::published: 0,612 schedFixed::scheduler::publishedBy: Set(),613 schedFixed::scheduler::ws:614 Map(615 "w1" ->616 {617 attached: Set(),618 built: false,619 expecting: false,620 running: false,621 session: true,622 up: true623 },624 "w2" ->625 {626 attached: Set(),627 built: false,628 expecting: false,629 running: false,630 session: true,631 up: true632 }633 )634}635636[State 16]637{638 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),639 schedFixed::scheduler::crashes: 2,640 schedFixed::scheduler::entry:641 [{ followers: Set("c2"), leased: true, worker: "w2" }],642 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),643 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),644 schedFixed::scheduler::mBuild: Set(("c2", "w1")),645 schedFixed::scheduler::mDone: Set(),646 schedFixed::scheduler::mExpect: Set("w2"),647 schedFixed::scheduler::mResult: Set(),648 schedFixed::scheduler::mRetry: Set("c1"),649 schedFixed::scheduler::mRevoke: Set(),650 schedFixed::scheduler::mSchedule: Set("c1"),651 schedFixed::scheduler::published: 0,652 schedFixed::scheduler::publishedBy: Set(),653 schedFixed::scheduler::ws:654 Map(655 "w1" ->656 {657 attached: Set(),658 built: false,659 expecting: false,660 running: false,661 session: true,662 up: true663 },664 "w2" ->665 {666 attached: Set(),667 built: false,668 expecting: false,669 running: false,670 session: true,671 up: true672 }673 )674}675676[State 17]677{678 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),679 schedFixed::scheduler::crashes: 2,680 schedFixed::scheduler::entry:681 [{ followers: Set("c2"), leased: true, worker: "w2" }],682 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),683 schedFixed::scheduler::mAssigned: Set(),684 schedFixed::scheduler::mBuild: Set(("c2", "w1"), ("c2", "w2")),685 schedFixed::scheduler::mDone: Set(),686 schedFixed::scheduler::mExpect: Set("w2"),687 schedFixed::scheduler::mResult: Set(),688 schedFixed::scheduler::mRetry: Set("c1"),689 schedFixed::scheduler::mRevoke: Set(),690 schedFixed::scheduler::mSchedule: Set("c1"),691 schedFixed::scheduler::published: 0,692 schedFixed::scheduler::publishedBy: Set(),693 schedFixed::scheduler::ws:694 Map(695 "w1" ->696 {697 attached: Set(),698 built: false,699 expecting: false,700 running: false,701 session: true,702 up: true703 },704 "w2" ->705 {706 attached: Set(),707 built: false,708 expecting: false,709 running: false,710 session: true,711 up: true712 }713 )714}715716[State 18]717{718 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),719 schedFixed::scheduler::crashes: 2,720 schedFixed::scheduler::entry:721 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],722 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),723 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),724 schedFixed::scheduler::mBuild: Set(("c2", "w1"), ("c2", "w2")),725 schedFixed::scheduler::mDone: Set(),726 schedFixed::scheduler::mExpect: Set("w2"),727 schedFixed::scheduler::mResult: Set(),728 schedFixed::scheduler::mRetry: Set("c1"),729 schedFixed::scheduler::mRevoke: Set(),730 schedFixed::scheduler::mSchedule: Set(),731 schedFixed::scheduler::published: 0,732 schedFixed::scheduler::publishedBy: Set(),733 schedFixed::scheduler::ws:734 Map(735 "w1" ->736 {737 attached: Set(),738 built: false,739 expecting: false,740 running: false,741 session: true,742 up: true743 },744 "w2" ->745 {746 attached: Set(),747 built: false,748 expecting: false,749 running: false,750 session: true,751 up: true752 }753 )754}755756[State 19]757{758 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),759 schedFixed::scheduler::crashes: 2,760 schedFixed::scheduler::entry:761 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],762 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),763 schedFixed::scheduler::mAssigned: Set(),764 schedFixed::scheduler::mBuild: Set(("c2", "w1"), ("c2", "w2")),765 schedFixed::scheduler::mDone: Set(),766 schedFixed::scheduler::mExpect: Set("w2"),767 schedFixed::scheduler::mResult: Set(),768 schedFixed::scheduler::mRetry: Set(),769 schedFixed::scheduler::mRevoke: Set(),770 schedFixed::scheduler::mSchedule: Set("c1"),771 schedFixed::scheduler::published: 0,772 schedFixed::scheduler::publishedBy: Set(),773 schedFixed::scheduler::ws:774 Map(775 "w1" ->776 {777 attached: Set(),778 built: false,779 expecting: false,780 running: false,781 session: true,782 up: true783 },784 "w2" ->785 {786 attached: Set(),787 built: false,788 expecting: false,789 running: false,790 session: true,791 up: true792 }793 )794}795796[State 20]797{798 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),799 schedFixed::scheduler::crashes: 2,800 schedFixed::scheduler::entry:801 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],802 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),803 schedFixed::scheduler::mAssigned: Set(),804 schedFixed::scheduler::mBuild: Set(("c2", "w2")),805 schedFixed::scheduler::mDone: Set(),806 schedFixed::scheduler::mExpect: Set("w2"),807 schedFixed::scheduler::mResult: Set(),808 schedFixed::scheduler::mRetry: Set("c2"),809 schedFixed::scheduler::mRevoke: Set(),810 schedFixed::scheduler::mSchedule: Set("c1"),811 schedFixed::scheduler::published: 0,812 schedFixed::scheduler::publishedBy: Set(),813 schedFixed::scheduler::ws:814 Map(815 "w1" ->816 {817 attached: Set(),818 built: false,819 expecting: false,820 running: false,821 session: true,822 up: true823 },824 "w2" ->825 {826 attached: Set(),827 built: false,828 expecting: false,829 running: false,830 session: true,831 up: true832 }833 )834}835836[State 21]837{838 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),839 schedFixed::scheduler::crashes: 2,840 schedFixed::scheduler::entry:841 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],842 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),843 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),844 schedFixed::scheduler::mBuild: Set(("c2", "w2")),845 schedFixed::scheduler::mDone: Set(),846 schedFixed::scheduler::mExpect: Set("w2"),847 schedFixed::scheduler::mResult: Set(),848 schedFixed::scheduler::mRetry: Set("c2"),849 schedFixed::scheduler::mRevoke: Set(),850 schedFixed::scheduler::mSchedule: Set(),851 schedFixed::scheduler::published: 0,852 schedFixed::scheduler::publishedBy: Set(),853 schedFixed::scheduler::ws:854 Map(855 "w1" ->856 {857 attached: Set(),858 built: false,859 expecting: false,860 running: false,861 session: true,862 up: true863 },864 "w2" ->865 {866 attached: Set(),867 built: false,868 expecting: false,869 running: false,870 session: true,871 up: true872 }873 )874}875876[State 22]877{878 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),879 schedFixed::scheduler::crashes: 2,880 schedFixed::scheduler::entry:881 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],882 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),883 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),884 schedFixed::scheduler::mBuild: Set(("c2", "w2")),885 schedFixed::scheduler::mDone: Set(),886 schedFixed::scheduler::mExpect: Set(),887 schedFixed::scheduler::mResult: Set(),888 schedFixed::scheduler::mRetry: Set("c2"),889 schedFixed::scheduler::mRevoke: Set(),890 schedFixed::scheduler::mSchedule: Set(),891 schedFixed::scheduler::published: 0,892 schedFixed::scheduler::publishedBy: Set(),893 schedFixed::scheduler::ws:894 Map(895 "w1" ->896 {897 attached: Set(),898 built: false,899 expecting: false,900 running: false,901 session: true,902 up: true903 },904 "w2" ->905 {906 attached: Set(),907 built: false,908 expecting: true,909 running: true,910 session: true,911 up: true912 }913 )914}915916[State 23]917{918 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),919 schedFixed::scheduler::crashes: 2,920 schedFixed::scheduler::entry:921 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],922 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),923 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),924 schedFixed::scheduler::mBuild: Set(("c2", "w2")),925 schedFixed::scheduler::mDone: Set(),926 schedFixed::scheduler::mExpect: Set(),927 schedFixed::scheduler::mResult: Set(),928 schedFixed::scheduler::mRetry: Set(),929 schedFixed::scheduler::mRevoke: Set(),930 schedFixed::scheduler::mSchedule: Set("c2"),931 schedFixed::scheduler::published: 0,932 schedFixed::scheduler::publishedBy: Set(),933 schedFixed::scheduler::ws:934 Map(935 "w1" ->936 {937 attached: Set(),938 built: false,939 expecting: false,940 running: false,941 session: true,942 up: true943 },944 "w2" ->945 {946 attached: Set(),947 built: false,948 expecting: true,949 running: true,950 session: true,951 up: true952 }953 )954}955956[State 24]957{958 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),959 schedFixed::scheduler::crashes: 2,960 schedFixed::scheduler::entry:961 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],962 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),963 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),964 schedFixed::scheduler::mBuild: Set(("c2", "w2")),965 schedFixed::scheduler::mDone: Set("w2"),966 schedFixed::scheduler::mExpect: Set(),967 schedFixed::scheduler::mResult: Set(),968 schedFixed::scheduler::mRetry: Set(),969 schedFixed::scheduler::mRevoke: Set(),970 schedFixed::scheduler::mSchedule: Set("c2"),971 schedFixed::scheduler::published: 1,972 schedFixed::scheduler::publishedBy: Set("w2"),973 schedFixed::scheduler::ws:974 Map(975 "w1" ->976 {977 attached: Set(),978 built: false,979 expecting: false,980 running: false,981 session: true,982 up: true983 },984 "w2" ->985 {986 attached: Set(),987 built: true,988 expecting: false,989 running: false,990 session: true,991 up: true992 }993 )994}995996[State 25]997{998 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),999 schedFixed::scheduler::crashes: 2,1000 schedFixed::scheduler::entry:1001 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1002 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1003 schedFixed::scheduler::mAssigned: Set(),1004 schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),1005 schedFixed::scheduler::mDone: Set("w2"),1006 schedFixed::scheduler::mExpect: Set(),1007 schedFixed::scheduler::mResult: Set(),1008 schedFixed::scheduler::mRetry: Set(),1009 schedFixed::scheduler::mRevoke: Set(),1010 schedFixed::scheduler::mSchedule: Set("c2"),1011 schedFixed::scheduler::published: 1,1012 schedFixed::scheduler::publishedBy: Set("w2"),1013 schedFixed::scheduler::ws:1014 Map(1015 "w1" ->1016 {1017 attached: Set(),1018 built: false,1019 expecting: false,1020 running: false,1021 session: true,1022 up: true1023 },1024 "w2" ->1025 {1026 attached: Set(),1027 built: true,1028 expecting: false,1029 running: false,1030 session: true,1031 up: true1032 }1033 )1034}10351036[State 26]1037{1038 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),1039 schedFixed::scheduler::crashes: 2,1040 schedFixed::scheduler::entry:1041 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1042 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1043 schedFixed::scheduler::mAssigned: Set(),1044 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1045 schedFixed::scheduler::mDone: Set("w2"),1046 schedFixed::scheduler::mExpect: Set(),1047 schedFixed::scheduler::mResult: Set("c1"),1048 schedFixed::scheduler::mRetry: Set(),1049 schedFixed::scheduler::mRevoke: Set(),1050 schedFixed::scheduler::mSchedule: Set("c2"),1051 schedFixed::scheduler::published: 1,1052 schedFixed::scheduler::publishedBy: Set("w2"),1053 schedFixed::scheduler::ws:1054 Map(1055 "w1" ->1056 {1057 attached: Set(),1058 built: false,1059 expecting: false,1060 running: false,1061 session: true,1062 up: true1063 },1064 "w2" ->1065 {1066 attached: Set(),1067 built: true,1068 expecting: false,1069 running: false,1070 session: true,1071 up: true1072 }1073 )1074}10751076[State 27]1077{1078 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),1079 schedFixed::scheduler::crashes: 2,1080 schedFixed::scheduler::entry:1081 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1082 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1083 schedFixed::scheduler::mAssigned: Set(),1084 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1085 schedFixed::scheduler::mDone: Set("w2"),1086 schedFixed::scheduler::mExpect: Set(),1087 schedFixed::scheduler::mResult: Set("c1", "c2"),1088 schedFixed::scheduler::mRetry: Set(),1089 schedFixed::scheduler::mRevoke: Set(),1090 schedFixed::scheduler::mSchedule: Set(),1091 schedFixed::scheduler::published: 1,1092 schedFixed::scheduler::publishedBy: Set("w2"),1093 schedFixed::scheduler::ws:1094 Map(1095 "w1" ->1096 {1097 attached: Set(),1098 built: false,1099 expecting: false,1100 running: false,1101 session: true,1102 up: true1103 },1104 "w2" ->1105 {1106 attached: Set(),1107 built: true,1108 expecting: false,1109 running: false,1110 session: true,1111 up: true1112 }1113 )1114}11151116[State 28]1117{1118 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CQueued),1119 schedFixed::scheduler::crashes: 2,1120 schedFixed::scheduler::entry:1121 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1122 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1123 schedFixed::scheduler::mAssigned: Set(),1124 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1125 schedFixed::scheduler::mDone: Set("w2"),1126 schedFixed::scheduler::mExpect: Set(),1127 schedFixed::scheduler::mResult: Set("c2"),1128 schedFixed::scheduler::mRetry: Set(),1129 schedFixed::scheduler::mRevoke: Set(),1130 schedFixed::scheduler::mSchedule: Set(),1131 schedFixed::scheduler::published: 1,1132 schedFixed::scheduler::publishedBy: Set("w2"),1133 schedFixed::scheduler::ws:1134 Map(1135 "w1" ->1136 {1137 attached: Set(),1138 built: false,1139 expecting: false,1140 running: false,1141 session: true,1142 up: true1143 },1144 "w2" ->1145 {1146 attached: Set(),1147 built: true,1148 expecting: false,1149 running: false,1150 session: true,1151 up: true1152 }1153 )1154}11551156[State 29]1157{1158 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1159 schedFixed::scheduler::crashes: 2,1160 schedFixed::scheduler::entry:1161 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],1162 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),1163 schedFixed::scheduler::mAssigned: Set(),1164 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1165 schedFixed::scheduler::mDone: Set("w2"),1166 schedFixed::scheduler::mExpect: Set(),1167 schedFixed::scheduler::mResult: Set(),1168 schedFixed::scheduler::mRetry: Set(),1169 schedFixed::scheduler::mRevoke: Set(),1170 schedFixed::scheduler::mSchedule: Set(),1171 schedFixed::scheduler::published: 1,1172 schedFixed::scheduler::publishedBy: Set("w2"),1173 schedFixed::scheduler::ws:1174 Map(1175 "w1" ->1176 {1177 attached: Set(),1178 built: false,1179 expecting: false,1180 running: false,1181 session: true,1182 up: true1183 },1184 "w2" ->1185 {1186 attached: Set(),1187 built: true,1188 expecting: false,1189 running: false,1190 session: true,1191 up: true1192 }1193 )1194}11951196[State 30]1197{1198 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1199 schedFixed::scheduler::crashes: 2,1200 schedFixed::scheduler::entry: [],1201 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1202 schedFixed::scheduler::mAssigned: Set(),1203 schedFixed::scheduler::mBuild: Set(("c2", "w2")),1204 schedFixed::scheduler::mDone: Set(),1205 schedFixed::scheduler::mExpect: Set(),1206 schedFixed::scheduler::mResult: Set(),1207 schedFixed::scheduler::mRetry: Set(),1208 schedFixed::scheduler::mRevoke: Set(),1209 schedFixed::scheduler::mSchedule: Set(),1210 schedFixed::scheduler::published: 1,1211 schedFixed::scheduler::publishedBy: Set("w2"),1212 schedFixed::scheduler::ws:1213 Map(1214 "w1" ->1215 {1216 attached: Set(),1217 built: false,1218 expecting: false,1219 running: false,1220 session: true,1221 up: true1222 },1223 "w2" ->1224 {1225 attached: Set(),1226 built: true,1227 expecting: false,1228 running: false,1229 session: true,1230 up: true1231 }1232 )1233}12341235[ok] No violation found (4784ms at 6271 traces/second).1236Trace length statistics: max=31, min=15, average=18.721237You may increase --max-samples and --max-steps.1238Use --verbosity to produce more (or less) output.1239Use --seed=0x45e34c16836e765c --backend=rust to reproduce.1240An example execution:12411242[State 0]1243{1244 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1245 schedNoRevoke::scheduler::crashes: 0,1246 schedNoRevoke::scheduler::entry: [],1247 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1248 schedNoRevoke::scheduler::mAssigned: Set(),1249 schedNoRevoke::scheduler::mBuild: Set(),1250 schedNoRevoke::scheduler::mDone: Set(),1251 schedNoRevoke::scheduler::mExpect: Set(),1252 schedNoRevoke::scheduler::mResult: Set(),1253 schedNoRevoke::scheduler::mRetry: Set(),1254 schedNoRevoke::scheduler::mRevoke: Set(),1255 schedNoRevoke::scheduler::mSchedule: Set(),1256 schedNoRevoke::scheduler::published: 0,1257 schedNoRevoke::scheduler::publishedBy: Set(),1258 schedNoRevoke::scheduler::ws:1259 Map(1260 "w1" ->1261 {1262 attached: Set(),1263 built: false,1264 expecting: false,1265 running: false,1266 session: true,1267 up: true1268 },1269 "w2" ->1270 {1271 attached: Set(),1272 built: false,1273 expecting: false,1274 running: false,1275 session: true,1276 up: true1277 }1278 )1279}12801281[State 1]1282{1283 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1284 schedNoRevoke::scheduler::crashes: 1,1285 schedNoRevoke::scheduler::entry: [],1286 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1287 schedNoRevoke::scheduler::mAssigned: Set(),1288 schedNoRevoke::scheduler::mBuild: Set(),1289 schedNoRevoke::scheduler::mDone: Set(),1290 schedNoRevoke::scheduler::mExpect: Set(),1291 schedNoRevoke::scheduler::mResult: Set(),1292 schedNoRevoke::scheduler::mRetry: Set(),1293 schedNoRevoke::scheduler::mRevoke: Set(),1294 schedNoRevoke::scheduler::mSchedule: Set(),1295 schedNoRevoke::scheduler::published: 0,1296 schedNoRevoke::scheduler::publishedBy: Set(),1297 schedNoRevoke::scheduler::ws:1298 Map(1299 "w1" ->1300 {1301 attached: Set(),1302 built: false,1303 expecting: false,1304 running: false,1305 session: false,1306 up: false1307 },1308 "w2" ->1309 {1310 attached: Set(),1311 built: false,1312 expecting: false,1313 running: false,1314 session: true,1315 up: true1316 }1317 )1318}13191320[State 2]1321{1322 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1323 schedNoRevoke::scheduler::crashes: 1,1324 schedNoRevoke::scheduler::entry: [],1325 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1326 schedNoRevoke::scheduler::mAssigned: Set(),1327 schedNoRevoke::scheduler::mBuild: Set(),1328 schedNoRevoke::scheduler::mDone: Set(),1329 schedNoRevoke::scheduler::mExpect: Set(),1330 schedNoRevoke::scheduler::mResult: Set(),1331 schedNoRevoke::scheduler::mRetry: Set(),1332 schedNoRevoke::scheduler::mRevoke: Set(),1333 schedNoRevoke::scheduler::mSchedule: Set("c1"),1334 schedNoRevoke::scheduler::published: 0,1335 schedNoRevoke::scheduler::publishedBy: Set(),1336 schedNoRevoke::scheduler::ws:1337 Map(1338 "w1" ->1339 {1340 attached: Set(),1341 built: false,1342 expecting: false,1343 running: false,1344 session: false,1345 up: false1346 },1347 "w2" ->1348 {1349 attached: Set(),1350 built: false,1351 expecting: false,1352 running: false,1353 session: true,1354 up: true1355 }1356 )1357}13581359[State 3]1360{1361 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1362 schedNoRevoke::scheduler::crashes: 1,1363 schedNoRevoke::scheduler::entry:1364 [{ followers: Set("c1"), leased: true, worker: "w2" }],1365 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1366 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1367 schedNoRevoke::scheduler::mBuild: Set(),1368 schedNoRevoke::scheduler::mDone: Set(),1369 schedNoRevoke::scheduler::mExpect: Set("w2"),1370 schedNoRevoke::scheduler::mResult: Set(),1371 schedNoRevoke::scheduler::mRetry: Set(),1372 schedNoRevoke::scheduler::mRevoke: Set(),1373 schedNoRevoke::scheduler::mSchedule: Set(),1374 schedNoRevoke::scheduler::published: 0,1375 schedNoRevoke::scheduler::publishedBy: Set(),1376 schedNoRevoke::scheduler::ws:1377 Map(1378 "w1" ->1379 {1380 attached: Set(),1381 built: false,1382 expecting: false,1383 running: false,1384 session: false,1385 up: false1386 },1387 "w2" ->1388 {1389 attached: Set(),1390 built: false,1391 expecting: false,1392 running: false,1393 session: true,1394 up: true1395 }1396 )1397}13981399[State 4]1400{1401 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1402 schedNoRevoke::scheduler::crashes: 1,1403 schedNoRevoke::scheduler::entry:1404 [{ followers: Set("c1"), leased: true, worker: "w2" }],1405 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1406 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1407 schedNoRevoke::scheduler::mBuild: Set(),1408 schedNoRevoke::scheduler::mDone: Set(),1409 schedNoRevoke::scheduler::mExpect: Set(),1410 schedNoRevoke::scheduler::mResult: Set(),1411 schedNoRevoke::scheduler::mRetry: Set(),1412 schedNoRevoke::scheduler::mRevoke: Set(),1413 schedNoRevoke::scheduler::mSchedule: Set(),1414 schedNoRevoke::scheduler::published: 0,1415 schedNoRevoke::scheduler::publishedBy: Set(),1416 schedNoRevoke::scheduler::ws:1417 Map(1418 "w1" ->1419 {1420 attached: Set(),1421 built: false,1422 expecting: false,1423 running: false,1424 session: false,1425 up: false1426 },1427 "w2" ->1428 {1429 attached: Set(),1430 built: false,1431 expecting: true,1432 running: true,1433 session: true,1434 up: true1435 }1436 )1437}14381439[State 5]1440{1441 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1442 schedNoRevoke::scheduler::crashes: 2,1443 schedNoRevoke::scheduler::entry: [],1444 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1445 schedNoRevoke::scheduler::mAssigned: Set(),1446 schedNoRevoke::scheduler::mBuild: Set(),1447 schedNoRevoke::scheduler::mDone: Set(),1448 schedNoRevoke::scheduler::mExpect: Set(),1449 schedNoRevoke::scheduler::mResult: Set(),1450 schedNoRevoke::scheduler::mRetry: Set("c1"),1451 schedNoRevoke::scheduler::mRevoke: Set(),1452 schedNoRevoke::scheduler::mSchedule: Set(),1453 schedNoRevoke::scheduler::published: 0,1454 schedNoRevoke::scheduler::publishedBy: Set(),1455 schedNoRevoke::scheduler::ws:1456 Map(1457 "w1" ->1458 {1459 attached: Set(),1460 built: false,1461 expecting: false,1462 running: false,1463 session: false,1464 up: false1465 },1466 "w2" ->1467 {1468 attached: Set(),1469 built: false,1470 expecting: true,1471 running: true,1472 session: false,1473 up: true1474 }1475 )1476}14771478[State 6]1479{1480 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1481 schedNoRevoke::scheduler::crashes: 2,1482 schedNoRevoke::scheduler::entry: [],1483 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1484 schedNoRevoke::scheduler::mAssigned: Set(),1485 schedNoRevoke::scheduler::mBuild: Set(),1486 schedNoRevoke::scheduler::mDone: Set(),1487 schedNoRevoke::scheduler::mExpect: Set(),1488 schedNoRevoke::scheduler::mResult: Set(),1489 schedNoRevoke::scheduler::mRetry: Set(),1490 schedNoRevoke::scheduler::mRevoke: Set(),1491 schedNoRevoke::scheduler::mSchedule: Set("c1"),1492 schedNoRevoke::scheduler::published: 0,1493 schedNoRevoke::scheduler::publishedBy: Set(),1494 schedNoRevoke::scheduler::ws:1495 Map(1496 "w1" ->1497 {1498 attached: Set(),1499 built: false,1500 expecting: false,1501 running: false,1502 session: false,1503 up: false1504 },1505 "w2" ->1506 {1507 attached: Set(),1508 built: false,1509 expecting: true,1510 running: true,1511 session: false,1512 up: true1513 }1514 )1515}15161517[State 7]1518{1519 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1520 schedNoRevoke::scheduler::crashes: 2,1521 schedNoRevoke::scheduler::entry: [],1522 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1523 schedNoRevoke::scheduler::mAssigned: Set(),1524 schedNoRevoke::scheduler::mBuild: Set(),1525 schedNoRevoke::scheduler::mDone: Set(),1526 schedNoRevoke::scheduler::mExpect: Set(),1527 schedNoRevoke::scheduler::mResult: Set(),1528 schedNoRevoke::scheduler::mRetry: Set(),1529 schedNoRevoke::scheduler::mRevoke: Set(),1530 schedNoRevoke::scheduler::mSchedule: Set("c1"),1531 schedNoRevoke::scheduler::published: 0,1532 schedNoRevoke::scheduler::publishedBy: Set(),1533 schedNoRevoke::scheduler::ws:1534 Map(1535 "w1" ->1536 {1537 attached: Set(),1538 built: false,1539 expecting: false,1540 running: false,1541 session: true,1542 up: true1543 },1544 "w2" ->1545 {1546 attached: Set(),1547 built: false,1548 expecting: true,1549 running: true,1550 session: false,1551 up: true1552 }1553 )1554}15551556[State 8]1557{1558 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1559 schedNoRevoke::scheduler::crashes: 2,1560 schedNoRevoke::scheduler::entry:1561 [{ followers: Set("c1"), leased: true, worker: "w1" }],1562 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1563 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1564 schedNoRevoke::scheduler::mBuild: Set(),1565 schedNoRevoke::scheduler::mDone: Set(),1566 schedNoRevoke::scheduler::mExpect: Set("w1"),1567 schedNoRevoke::scheduler::mResult: Set(),1568 schedNoRevoke::scheduler::mRetry: Set(),1569 schedNoRevoke::scheduler::mRevoke: Set(),1570 schedNoRevoke::scheduler::mSchedule: Set(),1571 schedNoRevoke::scheduler::published: 0,1572 schedNoRevoke::scheduler::publishedBy: Set(),1573 schedNoRevoke::scheduler::ws:1574 Map(1575 "w1" ->1576 {1577 attached: Set(),1578 built: false,1579 expecting: false,1580 running: false,1581 session: true,1582 up: true1583 },1584 "w2" ->1585 {1586 attached: Set(),1587 built: false,1588 expecting: true,1589 running: true,1590 session: false,1591 up: true1592 }1593 )1594}15951596[State 9]1597{1598 schedNoRevoke::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),1599 schedNoRevoke::scheduler::crashes: 2,1600 schedNoRevoke::scheduler::entry:1601 [{ followers: Set("c1"), leased: true, worker: "w1" }],1602 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1603 schedNoRevoke::scheduler::mAssigned: Set(),1604 schedNoRevoke::scheduler::mBuild: Set(("c1", "w1")),1605 schedNoRevoke::scheduler::mDone: Set(),1606 schedNoRevoke::scheduler::mExpect: Set("w1"),1607 schedNoRevoke::scheduler::mResult: Set(),1608 schedNoRevoke::scheduler::mRetry: Set(),1609 schedNoRevoke::scheduler::mRevoke: Set(),1610 schedNoRevoke::scheduler::mSchedule: Set(),1611 schedNoRevoke::scheduler::published: 0,1612 schedNoRevoke::scheduler::publishedBy: Set(),1613 schedNoRevoke::scheduler::ws:1614 Map(1615 "w1" ->1616 {1617 attached: Set(),1618 built: false,1619 expecting: false,1620 running: false,1621 session: true,1622 up: true1623 },1624 "w2" ->1625 {1626 attached: Set(),1627 built: false,1628 expecting: true,1629 running: true,1630 session: false,1631 up: true1632 }1633 )1634}16351636[State 10]1637{1638 schedNoRevoke::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),1639 schedNoRevoke::scheduler::crashes: 2,1640 schedNoRevoke::scheduler::entry:1641 [{ followers: Set("c1"), leased: true, worker: "w1" }],1642 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1643 schedNoRevoke::scheduler::mAssigned: Set(),1644 schedNoRevoke::scheduler::mBuild: Set(("c1", "w1")),1645 schedNoRevoke::scheduler::mDone: Set(),1646 schedNoRevoke::scheduler::mExpect: Set("w1"),1647 schedNoRevoke::scheduler::mResult: Set(),1648 schedNoRevoke::scheduler::mRetry: Set(),1649 schedNoRevoke::scheduler::mRevoke: Set(),1650 schedNoRevoke::scheduler::mSchedule: Set(),1651 schedNoRevoke::scheduler::published: 0,1652 schedNoRevoke::scheduler::publishedBy: Set(),1653 schedNoRevoke::scheduler::ws:1654 Map(1655 "w1" ->1656 {1657 attached: Set(),1658 built: false,1659 expecting: false,1660 running: false,1661 session: true,1662 up: true1663 },1664 "w2" ->1665 {1666 attached: Set(),1667 built: false,1668 expecting: true,1669 running: true,1670 session: true,1671 up: true1672 }1673 )1674}16751676[State 11]1677{1678 schedNoRevoke::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),1679 schedNoRevoke::scheduler::crashes: 2,1680 schedNoRevoke::scheduler::entry:1681 [{ followers: Set("c1"), leased: true, worker: "w1" }],1682 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1683 schedNoRevoke::scheduler::mAssigned: Set(),1684 schedNoRevoke::scheduler::mBuild: Set(("c1", "w1")),1685 schedNoRevoke::scheduler::mDone: Set(),1686 schedNoRevoke::scheduler::mExpect: Set(),1687 schedNoRevoke::scheduler::mResult: Set(),1688 schedNoRevoke::scheduler::mRetry: Set(),1689 schedNoRevoke::scheduler::mRevoke: Set(),1690 schedNoRevoke::scheduler::mSchedule: Set(),1691 schedNoRevoke::scheduler::published: 0,1692 schedNoRevoke::scheduler::publishedBy: Set(),1693 schedNoRevoke::scheduler::ws:1694 Map(1695 "w1" ->1696 {1697 attached: Set(),1698 built: false,1699 expecting: true,1700 running: true,1701 session: true,1702 up: true1703 },1704 "w2" ->1705 {1706 attached: Set(),1707 built: false,1708 expecting: true,1709 running: true,1710 session: true,1711 up: true1712 }1713 )1714}17151716[violation] Found an issue (7266ms at 3878 traces/second).1717Use --verbosity=3 to show executions.1718Use --seed=0x8b3e78fc2d92a39e --backend=rust to reproduce.1719error: Invariant violated1720An example execution:17211722[State 0]1723{1724 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),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(),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 1]1762{1763 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1764 schedNoFence::scheduler::crashes: 0,1765 schedNoFence::scheduler::entry: [],1766 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1767 schedNoFence::scheduler::mAssigned: Set(),1768 schedNoFence::scheduler::mBuild: Set(),1769 schedNoFence::scheduler::mDone: Set(),1770 schedNoFence::scheduler::mExpect: Set(),1771 schedNoFence::scheduler::mResult: Set(),1772 schedNoFence::scheduler::mRetry: Set(),1773 schedNoFence::scheduler::mRevoke: Set(),1774 schedNoFence::scheduler::mSchedule: Set("c1"),1775 schedNoFence::scheduler::published: 0,1776 schedNoFence::scheduler::publishedBy: Set(),1777 schedNoFence::scheduler::ws:1778 Map(1779 "w1" ->1780 {1781 attached: Set(),1782 built: false,1783 expecting: false,1784 running: false,1785 session: true,1786 up: true1787 },1788 "w2" ->1789 {1790 attached: Set(),1791 built: false,1792 expecting: false,1793 running: false,1794 session: true,1795 up: true1796 }1797 )1798}17991800[State 2]1801{1802 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1803 schedNoFence::scheduler::crashes: 0,1804 schedNoFence::scheduler::entry:1805 [{ followers: Set("c1"), leased: true, worker: "w2" }],1806 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1807 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),1808 schedNoFence::scheduler::mBuild: Set(),1809 schedNoFence::scheduler::mDone: Set(),1810 schedNoFence::scheduler::mExpect: Set("w2"),1811 schedNoFence::scheduler::mResult: Set(),1812 schedNoFence::scheduler::mRetry: Set(),1813 schedNoFence::scheduler::mRevoke: Set(),1814 schedNoFence::scheduler::mSchedule: Set(),1815 schedNoFence::scheduler::published: 0,1816 schedNoFence::scheduler::publishedBy: Set(),1817 schedNoFence::scheduler::ws:1818 Map(1819 "w1" ->1820 {1821 attached: Set(),1822 built: false,1823 expecting: false,1824 running: false,1825 session: true,1826 up: true1827 },1828 "w2" ->1829 {1830 attached: Set(),1831 built: false,1832 expecting: false,1833 running: false,1834 session: true,1835 up: true1836 }1837 )1838}18391840[State 3]1841{1842 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1843 schedNoFence::scheduler::crashes: 0,1844 schedNoFence::scheduler::entry:1845 [{ followers: Set("c1"), leased: true, worker: "w2" }],1846 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),1847 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),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(),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: false,1864 running: false,1865 session: true,1866 up: true1867 },1868 "w2" ->1869 {1870 attached: Set(),1871 built: false,1872 expecting: true,1873 running: true,1874 session: true,1875 up: true1876 }1877 )1878}18791880[State 4]1881{1882 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),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("c1"),1892 schedNoFence::scheduler::mRevoke: Set(),1893 schedNoFence::scheduler::mSchedule: Set(),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: false,1903 running: false,1904 session: false,1905 up: true1906 },1907 "w2" ->1908 {1909 attached: Set(),1910 built: false,1911 expecting: true,1912 running: true,1913 session: false,1914 up: true1915 }1916 )1917}19181919[State 5]1920{1921 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),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("c1"),1931 schedNoFence::scheduler::mRevoke: Set(),1932 schedNoFence::scheduler::mSchedule: Set(),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: false,1942 running: false,1943 session: false,1944 up: false1945 },1946 "w2" ->1947 {1948 attached: Set(),1949 built: false,1950 expecting: true,1951 running: true,1952 session: false,1953 up: true1954 }1955 )1956}19571958[State 6]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("c1"),1970 schedNoFence::scheduler::mRevoke: Set(),1971 schedNoFence::scheduler::mSchedule: Set("c2"),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: false,1981 running: false,1982 session: false,1983 up: false1984 },1985 "w2" ->1986 {1987 attached: Set(),1988 built: false,1989 expecting: true,1990 running: true,1991 session: false,1992 up: true1993 }1994 )1995}19961997[State 7]1998{1999 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2000 schedNoFence::scheduler::crashes: 2,2001 schedNoFence::scheduler::entry: [],2002 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2003 schedNoFence::scheduler::mAssigned: Set(),2004 schedNoFence::scheduler::mBuild: Set(),2005 schedNoFence::scheduler::mDone: Set(),2006 schedNoFence::scheduler::mExpect: Set(),2007 schedNoFence::scheduler::mResult: Set(),2008 schedNoFence::scheduler::mRetry: Set("c1"),2009 schedNoFence::scheduler::mRevoke: Set(),2010 schedNoFence::scheduler::mSchedule: Set("c2"),2011 schedNoFence::scheduler::published: 0,2012 schedNoFence::scheduler::publishedBy: Set(),2013 schedNoFence::scheduler::ws:2014 Map(2015 "w1" ->2016 {2017 attached: Set(),2018 built: false,2019 expecting: false,2020 running: false,2021 session: true,2022 up: true2023 },2024 "w2" ->2025 {2026 attached: Set(),2027 built: false,2028 expecting: true,2029 running: true,2030 session: false,2031 up: true2032 }2033 )2034}20352036[State 8]2037{2038 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2039 schedNoFence::scheduler::crashes: 2,2040 schedNoFence::scheduler::entry:2041 [{ followers: Set("c2"), leased: true, worker: "w1" }],2042 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2043 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2044 schedNoFence::scheduler::mBuild: Set(),2045 schedNoFence::scheduler::mDone: Set(),2046 schedNoFence::scheduler::mExpect: Set("w1"),2047 schedNoFence::scheduler::mResult: Set(),2048 schedNoFence::scheduler::mRetry: Set("c1"),2049 schedNoFence::scheduler::mRevoke: Set(),2050 schedNoFence::scheduler::mSchedule: Set(),2051 schedNoFence::scheduler::published: 0,2052 schedNoFence::scheduler::publishedBy: Set(),2053 schedNoFence::scheduler::ws:2054 Map(2055 "w1" ->2056 {2057 attached: Set(),2058 built: false,2059 expecting: false,2060 running: false,2061 session: true,2062 up: true2063 },2064 "w2" ->2065 {2066 attached: Set(),2067 built: false,2068 expecting: true,2069 running: true,2070 session: false,2071 up: true2072 }2073 )2074}20752076[State 9]2077{2078 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2079 schedNoFence::scheduler::crashes: 2,2080 schedNoFence::scheduler::entry:2081 [{ followers: Set("c2"), leased: true, worker: "w1" }],2082 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2083 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2084 schedNoFence::scheduler::mBuild: Set(),2085 schedNoFence::scheduler::mDone: Set(),2086 schedNoFence::scheduler::mExpect: Set("w1"),2087 schedNoFence::scheduler::mResult: Set(),2088 schedNoFence::scheduler::mRetry: Set("c1"),2089 schedNoFence::scheduler::mRevoke: Set(),2090 schedNoFence::scheduler::mSchedule: Set(),2091 schedNoFence::scheduler::published: 1,2092 schedNoFence::scheduler::publishedBy: Set("w2"),2093 schedNoFence::scheduler::ws:2094 Map(2095 "w1" ->2096 {2097 attached: Set(),2098 built: false,2099 expecting: false,2100 running: false,2101 session: true,2102 up: true2103 },2104 "w2" ->2105 {2106 attached: Set(),2107 built: true,2108 expecting: false,2109 running: false,2110 session: false,2111 up: true2112 }2113 )2114}21152116[State 10]2117{2118 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2119 schedNoFence::scheduler::crashes: 2,2120 schedNoFence::scheduler::entry:2121 [{ followers: Set("c2"), leased: true, worker: "w1" }],2122 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2123 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2124 schedNoFence::scheduler::mBuild: Set(),2125 schedNoFence::scheduler::mDone: Set(),2126 schedNoFence::scheduler::mExpect: Set(),2127 schedNoFence::scheduler::mResult: Set(),2128 schedNoFence::scheduler::mRetry: Set("c1"),2129 schedNoFence::scheduler::mRevoke: Set(),2130 schedNoFence::scheduler::mSchedule: Set(),2131 schedNoFence::scheduler::published: 1,2132 schedNoFence::scheduler::publishedBy: Set("w2"),2133 schedNoFence::scheduler::ws:2134 Map(2135 "w1" ->2136 {2137 attached: Set(),2138 built: false,2139 expecting: true,2140 running: true,2141 session: true,2142 up: true2143 },2144 "w2" ->2145 {2146 attached: Set(),2147 built: true,2148 expecting: false,2149 running: false,2150 session: false,2151 up: true2152 }2153 )2154}21552156[State 11]2157{2158 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2159 schedNoFence::scheduler::crashes: 2,2160 schedNoFence::scheduler::entry:2161 [{ followers: Set("c2"), leased: true, worker: "w1" }],2162 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),2163 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),2164 schedNoFence::scheduler::mBuild: Set(),2165 schedNoFence::scheduler::mDone: Set("w1"),2166 schedNoFence::scheduler::mExpect: Set(),2167 schedNoFence::scheduler::mResult: Set(),2168 schedNoFence::scheduler::mRetry: Set("c1"),2169 schedNoFence::scheduler::mRevoke: Set(),2170 schedNoFence::scheduler::mSchedule: Set(),2171 schedNoFence::scheduler::published: 2,2172 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2173 schedNoFence::scheduler::ws:2174 Map(2175 "w1" ->2176 {2177 attached: Set(),2178 built: true,2179 expecting: false,2180 running: false,2181 session: true,2182 up: true2183 },2184 "w2" ->2185 {2186 attached: Set(),2187 built: true,2188 expecting: false,2189 running: false,2190 session: false,2191 up: true2192 }2193 )2194}21952196[violation] Found an issue (5873ms at 4393 traces/second).2197Use --verbosity=3 to show executions.2198Use --seed=0xfc20468d628a5abe --backend=rust to reproduce.2199error: Invariant violated2200An example execution:22012202[State 0]2203{2204 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2205 schedNoPush::scheduler::crashes: 0,2206 schedNoPush::scheduler::entry: [],2207 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2208 schedNoPush::scheduler::mAssigned: Set(),2209 schedNoPush::scheduler::mBuild: Set(),2210 schedNoPush::scheduler::mDone: Set(),2211 schedNoPush::scheduler::mExpect: Set(),2212 schedNoPush::scheduler::mResult: Set(),2213 schedNoPush::scheduler::mRetry: Set(),2214 schedNoPush::scheduler::mRevoke: Set(),2215 schedNoPush::scheduler::mSchedule: Set(),2216 schedNoPush::scheduler::published: 0,2217 schedNoPush::scheduler::publishedBy: Set(),2218 schedNoPush::scheduler::ws:2219 Map(2220 "w1" ->2221 {2222 attached: Set(),2223 built: false,2224 expecting: false,2225 running: false,2226 session: true,2227 up: true2228 },2229 "w2" ->2230 {2231 attached: Set(),2232 built: false,2233 expecting: false,2234 running: false,2235 session: true,2236 up: true2237 }2238 )2239}22402241[State 1]2242{2243 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2244 schedNoPush::scheduler::crashes: 0,2245 schedNoPush::scheduler::entry: [],2246 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2247 schedNoPush::scheduler::mAssigned: Set(),2248 schedNoPush::scheduler::mBuild: Set(),2249 schedNoPush::scheduler::mDone: Set(),2250 schedNoPush::scheduler::mExpect: Set(),2251 schedNoPush::scheduler::mResult: Set(),2252 schedNoPush::scheduler::mRetry: Set(),2253 schedNoPush::scheduler::mRevoke: Set(),2254 schedNoPush::scheduler::mSchedule: Set("c1"),2255 schedNoPush::scheduler::published: 0,2256 schedNoPush::scheduler::publishedBy: Set(),2257 schedNoPush::scheduler::ws:2258 Map(2259 "w1" ->2260 {2261 attached: Set(),2262 built: false,2263 expecting: false,2264 running: false,2265 session: true,2266 up: true2267 },2268 "w2" ->2269 {2270 attached: Set(),2271 built: false,2272 expecting: false,2273 running: false,2274 session: true,2275 up: true2276 }2277 )2278}22792280[State 2]2281{2282 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2283 schedNoPush::scheduler::crashes: 1,2284 schedNoPush::scheduler::entry: [],2285 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2286 schedNoPush::scheduler::mAssigned: Set(),2287 schedNoPush::scheduler::mBuild: Set(),2288 schedNoPush::scheduler::mDone: Set(),2289 schedNoPush::scheduler::mExpect: Set(),2290 schedNoPush::scheduler::mResult: Set(),2291 schedNoPush::scheduler::mRetry: Set(),2292 schedNoPush::scheduler::mRevoke: Set(),2293 schedNoPush::scheduler::mSchedule: Set("c1"),2294 schedNoPush::scheduler::published: 0,2295 schedNoPush::scheduler::publishedBy: Set(),2296 schedNoPush::scheduler::ws:2297 Map(2298 "w1" ->2299 {2300 attached: Set(),2301 built: false,2302 expecting: false,2303 running: false,2304 session: false,2305 up: false2306 },2307 "w2" ->2308 {2309 attached: Set(),2310 built: false,2311 expecting: false,2312 running: false,2313 session: true,2314 up: true2315 }2316 )2317}23182319[State 3]2320{2321 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2322 schedNoPush::scheduler::crashes: 1,2323 schedNoPush::scheduler::entry:2324 [{ followers: Set("c1"), leased: true, worker: "w2" }],2325 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2326 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2327 schedNoPush::scheduler::mBuild: Set(),2328 schedNoPush::scheduler::mDone: Set(),2329 schedNoPush::scheduler::mExpect: Set(),2330 schedNoPush::scheduler::mResult: Set(),2331 schedNoPush::scheduler::mRetry: Set(),2332 schedNoPush::scheduler::mRevoke: Set(),2333 schedNoPush::scheduler::mSchedule: Set(),2334 schedNoPush::scheduler::published: 0,2335 schedNoPush::scheduler::publishedBy: Set(),2336 schedNoPush::scheduler::ws:2337 Map(2338 "w1" ->2339 {2340 attached: Set(),2341 built: false,2342 expecting: false,2343 running: false,2344 session: false,2345 up: false2346 },2347 "w2" ->2348 {2349 attached: Set(),2350 built: false,2351 expecting: false,2352 running: false,2353 session: true,2354 up: true2355 }2356 )2357}23582359[State 4]2360{2361 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2362 schedNoPush::scheduler::crashes: 2,2363 schedNoPush::scheduler::entry:2364 [{ followers: Set("c1"), leased: true, worker: "w2" }],2365 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2366 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2367 schedNoPush::scheduler::mBuild: Set(),2368 schedNoPush::scheduler::mDone: Set(),2369 schedNoPush::scheduler::mExpect: Set(),2370 schedNoPush::scheduler::mResult: Set(),2371 schedNoPush::scheduler::mRetry: Set(),2372 schedNoPush::scheduler::mRevoke: Set(),2373 schedNoPush::scheduler::mSchedule: Set(),2374 schedNoPush::scheduler::published: 0,2375 schedNoPush::scheduler::publishedBy: Set(),2376 schedNoPush::scheduler::ws:2377 Map(2378 "w1" ->2379 {2380 attached: Set(),2381 built: false,2382 expecting: false,2383 running: false,2384 session: false,2385 up: false2386 },2387 "w2" ->2388 {2389 attached: Set(),2390 built: false,2391 expecting: false,2392 running: false,2393 session: false,2394 up: false2395 }2396 )2397}23982399[State 5]2400{2401 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2402 schedNoPush::scheduler::crashes: 2,2403 schedNoPush::scheduler::entry:2404 [{ followers: Set("c1"), leased: true, worker: "w2" }],2405 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2406 schedNoPush::scheduler::mAssigned: Set(),2407 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2408 schedNoPush::scheduler::mDone: Set(),2409 schedNoPush::scheduler::mExpect: Set(),2410 schedNoPush::scheduler::mResult: Set(),2411 schedNoPush::scheduler::mRetry: Set(),2412 schedNoPush::scheduler::mRevoke: Set(),2413 schedNoPush::scheduler::mSchedule: Set(),2414 schedNoPush::scheduler::published: 0,2415 schedNoPush::scheduler::publishedBy: Set(),2416 schedNoPush::scheduler::ws:2417 Map(2418 "w1" ->2419 {2420 attached: Set(),2421 built: false,2422 expecting: false,2423 running: false,2424 session: false,2425 up: false2426 },2427 "w2" ->2428 {2429 attached: Set(),2430 built: false,2431 expecting: false,2432 running: false,2433 session: false,2434 up: false2435 }2436 )2437}24382439[State 6]2440{2441 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2442 schedNoPush::scheduler::crashes: 2,2443 schedNoPush::scheduler::entry: [],2444 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2445 schedNoPush::scheduler::mAssigned: Set(),2446 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2447 schedNoPush::scheduler::mDone: Set(),2448 schedNoPush::scheduler::mExpect: Set(),2449 schedNoPush::scheduler::mResult: Set(),2450 schedNoPush::scheduler::mRetry: Set("c1"),2451 schedNoPush::scheduler::mRevoke: Set(),2452 schedNoPush::scheduler::mSchedule: Set(),2453 schedNoPush::scheduler::published: 0,2454 schedNoPush::scheduler::publishedBy: Set(),2455 schedNoPush::scheduler::ws:2456 Map(2457 "w1" ->2458 {2459 attached: Set(),2460 built: false,2461 expecting: false,2462 running: false,2463 session: false,2464 up: false2465 },2466 "w2" ->2467 {2468 attached: Set(),2469 built: false,2470 expecting: false,2471 running: false,2472 session: true,2473 up: true2474 }2475 )2476}24772478[State 7]2479{2480 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2481 schedNoPush::scheduler::crashes: 2,2482 schedNoPush::scheduler::entry: [],2483 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2484 schedNoPush::scheduler::mAssigned: Set(),2485 schedNoPush::scheduler::mBuild: Set(),2486 schedNoPush::scheduler::mDone: Set(),2487 schedNoPush::scheduler::mExpect: Set(),2488 schedNoPush::scheduler::mResult: Set(),2489 schedNoPush::scheduler::mRetry: Set("c1"),2490 schedNoPush::scheduler::mRevoke: Set(),2491 schedNoPush::scheduler::mSchedule: Set(),2492 schedNoPush::scheduler::published: 0,2493 schedNoPush::scheduler::publishedBy: Set(),2494 schedNoPush::scheduler::ws:2495 Map(2496 "w1" ->2497 {2498 attached: Set(),2499 built: false,2500 expecting: false,2501 running: false,2502 session: false,2503 up: false2504 },2505 "w2" ->2506 {2507 attached: Set("c1"),2508 built: false,2509 expecting: true,2510 running: true,2511 session: true,2512 up: true2513 }2514 )2515}25162517[violation] Found an issue (5462ms at 2384 traces/second).2518Use --verbosity=3 to show executions.2519Use --seed=0xd6246e4bd3823cc6 --backend=rust to reproduce.2520error: Invariant violated2521An example execution:25222523[State 0]2524{2525 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2526 schedNoReport::scheduler::crashes: 0,2527 schedNoReport::scheduler::entry: [],2528 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2529 schedNoReport::scheduler::mAssigned: Set(),2530 schedNoReport::scheduler::mBuild: Set(),2531 schedNoReport::scheduler::mDone: Set(),2532 schedNoReport::scheduler::mExpect: Set(),2533 schedNoReport::scheduler::mResult: Set(),2534 schedNoReport::scheduler::mRetry: Set(),2535 schedNoReport::scheduler::mRevoke: Set(),2536 schedNoReport::scheduler::mSchedule: Set(),2537 schedNoReport::scheduler::published: 0,2538 schedNoReport::scheduler::publishedBy: Set(),2539 schedNoReport::scheduler::ws:2540 Map(2541 "w1" ->2542 {2543 attached: Set(),2544 built: false,2545 expecting: false,2546 running: false,2547 session: true,2548 up: true2549 },2550 "w2" ->2551 {2552 attached: Set(),2553 built: false,2554 expecting: false,2555 running: false,2556 session: true,2557 up: true2558 }2559 )2560}25612562[State 1]2563{2564 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2565 schedNoReport::scheduler::crashes: 1,2566 schedNoReport::scheduler::entry: [],2567 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2568 schedNoReport::scheduler::mAssigned: Set(),2569 schedNoReport::scheduler::mBuild: Set(),2570 schedNoReport::scheduler::mDone: Set(),2571 schedNoReport::scheduler::mExpect: Set(),2572 schedNoReport::scheduler::mResult: Set(),2573 schedNoReport::scheduler::mRetry: Set(),2574 schedNoReport::scheduler::mRevoke: Set(),2575 schedNoReport::scheduler::mSchedule: Set(),2576 schedNoReport::scheduler::published: 0,2577 schedNoReport::scheduler::publishedBy: Set(),2578 schedNoReport::scheduler::ws:2579 Map(2580 "w1" ->2581 {2582 attached: Set(),2583 built: false,2584 expecting: false,2585 running: false,2586 session: true,2587 up: true2588 },2589 "w2" ->2590 {2591 attached: Set(),2592 built: false,2593 expecting: false,2594 running: false,2595 session: false,2596 up: false2597 }2598 )2599}26002601[State 2]2602{2603 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2604 schedNoReport::scheduler::crashes: 1,2605 schedNoReport::scheduler::entry: [],2606 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2607 schedNoReport::scheduler::mAssigned: Set(),2608 schedNoReport::scheduler::mBuild: Set(),2609 schedNoReport::scheduler::mDone: Set(),2610 schedNoReport::scheduler::mExpect: Set(),2611 schedNoReport::scheduler::mResult: Set(),2612 schedNoReport::scheduler::mRetry: Set(),2613 schedNoReport::scheduler::mRevoke: Set(),2614 schedNoReport::scheduler::mSchedule: Set("c2"),2615 schedNoReport::scheduler::published: 0,2616 schedNoReport::scheduler::publishedBy: Set(),2617 schedNoReport::scheduler::ws:2618 Map(2619 "w1" ->2620 {2621 attached: Set(),2622 built: false,2623 expecting: false,2624 running: false,2625 session: true,2626 up: true2627 },2628 "w2" ->2629 {2630 attached: Set(),2631 built: false,2632 expecting: false,2633 running: false,2634 session: false,2635 up: false2636 }2637 )2638}26392640[State 3]2641{2642 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2643 schedNoReport::scheduler::crashes: 1,2644 schedNoReport::scheduler::entry:2645 [{ followers: Set("c2"), leased: true, worker: "w1" }],2646 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2647 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2648 schedNoReport::scheduler::mBuild: Set(),2649 schedNoReport::scheduler::mDone: Set(),2650 schedNoReport::scheduler::mExpect: Set("w1"),2651 schedNoReport::scheduler::mResult: Set(),2652 schedNoReport::scheduler::mRetry: Set(),2653 schedNoReport::scheduler::mRevoke: Set(),2654 schedNoReport::scheduler::mSchedule: Set(),2655 schedNoReport::scheduler::published: 0,2656 schedNoReport::scheduler::publishedBy: Set(),2657 schedNoReport::scheduler::ws:2658 Map(2659 "w1" ->2660 {2661 attached: Set(),2662 built: false,2663 expecting: false,2664 running: false,2665 session: true,2666 up: true2667 },2668 "w2" ->2669 {2670 attached: Set(),2671 built: false,2672 expecting: false,2673 running: false,2674 session: false,2675 up: false2676 }2677 )2678}26792680[State 4]2681{2682 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2683 schedNoReport::scheduler::crashes: 1,2684 schedNoReport::scheduler::entry:2685 [{ followers: Set("c2"), leased: true, worker: "w1" }],2686 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2687 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2688 schedNoReport::scheduler::mBuild: Set(),2689 schedNoReport::scheduler::mDone: Set(),2690 schedNoReport::scheduler::mExpect: Set(),2691 schedNoReport::scheduler::mResult: Set(),2692 schedNoReport::scheduler::mRetry: Set(),2693 schedNoReport::scheduler::mRevoke: Set(),2694 schedNoReport::scheduler::mSchedule: Set(),2695 schedNoReport::scheduler::published: 0,2696 schedNoReport::scheduler::publishedBy: Set(),2697 schedNoReport::scheduler::ws:2698 Map(2699 "w1" ->2700 {2701 attached: Set(),2702 built: false,2703 expecting: true,2704 running: true,2705 session: true,2706 up: true2707 },2708 "w2" ->2709 {2710 attached: Set(),2711 built: false,2712 expecting: false,2713 running: false,2714 session: false,2715 up: false2716 }2717 )2718}27192720[State 5]2721{2722 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2723 schedNoReport::scheduler::crashes: 2,2724 schedNoReport::scheduler::entry: [],2725 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2726 schedNoReport::scheduler::mAssigned: Set(),2727 schedNoReport::scheduler::mBuild: Set(),2728 schedNoReport::scheduler::mDone: Set(),2729 schedNoReport::scheduler::mExpect: Set(),2730 schedNoReport::scheduler::mResult: Set(),2731 schedNoReport::scheduler::mRetry: Set("c2"),2732 schedNoReport::scheduler::mRevoke: Set(),2733 schedNoReport::scheduler::mSchedule: Set(),2734 schedNoReport::scheduler::published: 0,2735 schedNoReport::scheduler::publishedBy: Set(),2736 schedNoReport::scheduler::ws:2737 Map(2738 "w1" ->2739 {2740 attached: Set(),2741 built: false,2742 expecting: true,2743 running: true,2744 session: false,2745 up: true2746 },2747 "w2" ->2748 {2749 attached: Set(),2750 built: false,2751 expecting: false,2752 running: false,2753 session: false,2754 up: false2755 }2756 )2757}27582759[State 6]2760{2761 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2762 schedNoReport::scheduler::crashes: 2,2763 schedNoReport::scheduler::entry: [],2764 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2765 schedNoReport::scheduler::mAssigned: Set(),2766 schedNoReport::scheduler::mBuild: Set(),2767 schedNoReport::scheduler::mDone: Set(),2768 schedNoReport::scheduler::mExpect: Set(),2769 schedNoReport::scheduler::mResult: Set(),2770 schedNoReport::scheduler::mRetry: Set("c2"),2771 schedNoReport::scheduler::mRevoke: Set(),2772 schedNoReport::scheduler::mSchedule: Set(),2773 schedNoReport::scheduler::published: 0,2774 schedNoReport::scheduler::publishedBy: Set(),2775 schedNoReport::scheduler::ws:2776 Map(2777 "w1" ->2778 {2779 attached: Set(),2780 built: false,2781 expecting: true,2782 running: true,2783 session: false,2784 up: true2785 },2786 "w2" ->2787 {2788 attached: Set(),2789 built: false,2790 expecting: false,2791 running: false,2792 session: true,2793 up: true2794 }2795 )2796}27972798[State 7]2799{2800 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2801 schedNoReport::scheduler::crashes: 2,2802 schedNoReport::scheduler::entry: [],2803 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2804 schedNoReport::scheduler::mAssigned: Set(),2805 schedNoReport::scheduler::mBuild: Set(),2806 schedNoReport::scheduler::mDone: Set(),2807 schedNoReport::scheduler::mExpect: Set(),2808 schedNoReport::scheduler::mResult: Set(),2809 schedNoReport::scheduler::mRetry: Set("c2"),2810 schedNoReport::scheduler::mRevoke: Set(),2811 schedNoReport::scheduler::mSchedule: Set("c1"),2812 schedNoReport::scheduler::published: 0,2813 schedNoReport::scheduler::publishedBy: Set(),2814 schedNoReport::scheduler::ws:2815 Map(2816 "w1" ->2817 {2818 attached: Set(),2819 built: false,2820 expecting: true,2821 running: true,2822 session: false,2823 up: true2824 },2825 "w2" ->2826 {2827 attached: Set(),2828 built: false,2829 expecting: false,2830 running: false,2831 session: true,2832 up: true2833 }2834 )2835}28362837[State 8]2838{2839 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2840 schedNoReport::scheduler::crashes: 2,2841 schedNoReport::scheduler::entry:2842 [{ followers: Set("c1"), leased: true, worker: "w2" }],2843 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2844 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2845 schedNoReport::scheduler::mBuild: Set(),2846 schedNoReport::scheduler::mDone: Set(),2847 schedNoReport::scheduler::mExpect: Set("w2"),2848 schedNoReport::scheduler::mResult: Set(),2849 schedNoReport::scheduler::mRetry: Set("c2"),2850 schedNoReport::scheduler::mRevoke: Set(),2851 schedNoReport::scheduler::mSchedule: Set(),2852 schedNoReport::scheduler::published: 0,2853 schedNoReport::scheduler::publishedBy: Set(),2854 schedNoReport::scheduler::ws:2855 Map(2856 "w1" ->2857 {2858 attached: Set(),2859 built: false,2860 expecting: true,2861 running: true,2862 session: false,2863 up: true2864 },2865 "w2" ->2866 {2867 attached: Set(),2868 built: false,2869 expecting: false,2870 running: false,2871 session: true,2872 up: true2873 }2874 )2875}28762877[State 9]2878{2879 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2880 schedNoReport::scheduler::crashes: 2,2881 schedNoReport::scheduler::entry:2882 [{ followers: Set("c1"), leased: true, worker: "w2" }],2883 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2884 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2885 schedNoReport::scheduler::mBuild: Set(),2886 schedNoReport::scheduler::mDone: Set(),2887 schedNoReport::scheduler::mExpect: Set("w2"),2888 schedNoReport::scheduler::mResult: Set(),2889 schedNoReport::scheduler::mRetry: Set("c2"),2890 schedNoReport::scheduler::mRevoke: Set(),2891 schedNoReport::scheduler::mSchedule: Set(),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: true,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 10]2918{2919 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2920 schedNoReport::scheduler::crashes: 2,2921 schedNoReport::scheduler::entry:2922 [{ followers: Set("c1"), leased: true, worker: "w2" }],2923 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2924 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2925 schedNoReport::scheduler::mBuild: Set(),2926 schedNoReport::scheduler::mDone: Set(),2927 schedNoReport::scheduler::mExpect: Set(),2928 schedNoReport::scheduler::mResult: Set(),2929 schedNoReport::scheduler::mRetry: Set("c2"),2930 schedNoReport::scheduler::mRevoke: Set(),2931 schedNoReport::scheduler::mSchedule: Set(),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: true,2943 up: true2944 },2945 "w2" ->2946 {2947 attached: Set(),2948 built: false,2949 expecting: true,2950 running: true,2951 session: true,2952 up: true2953 }2954 )2955}29562957[violation] Found an issue (5820ms at 3890 traces/second).2958Use --verbosity=3 to show executions.2959Use --seed=0x2042f0aeee330f76 --backend=rust to reproduce.2960error: Invariant violated2961An example execution:29622963[State 0]2964{2965 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2966 schedTerminal::scheduler::crashes: 0,2967 schedTerminal::scheduler::entry: [],2968 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2969 schedTerminal::scheduler::mAssigned: Set(),2970 schedTerminal::scheduler::mBuild: Set(),2971 schedTerminal::scheduler::mDone: Set(),2972 schedTerminal::scheduler::mExpect: Set(),2973 schedTerminal::scheduler::mResult: Set(),2974 schedTerminal::scheduler::mRetry: Set(),2975 schedTerminal::scheduler::mRevoke: Set(),2976 schedTerminal::scheduler::mSchedule: Set(),2977 schedTerminal::scheduler::published: 0,2978 schedTerminal::scheduler::publishedBy: Set(),2979 schedTerminal::scheduler::ws:2980 Map(2981 "w1" ->2982 {2983 attached: Set(),2984 built: false,2985 expecting: false,2986 running: false,2987 session: true,2988 up: true2989 },2990 "w2" ->2991 {2992 attached: Set(),2993 built: false,2994 expecting: false,2995 running: false,2996 session: true,2997 up: true2998 }2999 )3000}30013002[State 1]3003{3004 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3005 schedTerminal::scheduler::crashes: 1,3006 schedTerminal::scheduler::entry: [],3007 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3008 schedTerminal::scheduler::mAssigned: Set(),3009 schedTerminal::scheduler::mBuild: Set(),3010 schedTerminal::scheduler::mDone: Set(),3011 schedTerminal::scheduler::mExpect: Set(),3012 schedTerminal::scheduler::mResult: Set(),3013 schedTerminal::scheduler::mRetry: Set(),3014 schedTerminal::scheduler::mRevoke: Set(),3015 schedTerminal::scheduler::mSchedule: Set(),3016 schedTerminal::scheduler::published: 0,3017 schedTerminal::scheduler::publishedBy: Set(),3018 schedTerminal::scheduler::ws:3019 Map(3020 "w1" ->3021 {3022 attached: Set(),3023 built: false,3024 expecting: false,3025 running: false,3026 session: false,3027 up: true3028 },3029 "w2" ->3030 {3031 attached: Set(),3032 built: false,3033 expecting: false,3034 running: false,3035 session: false,3036 up: true3037 }3038 )3039}30403041[State 2]3042{3043 schedTerminal::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),3044 schedTerminal::scheduler::crashes: 1,3045 schedTerminal::scheduler::entry: [],3046 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3047 schedTerminal::scheduler::mAssigned: Set(),3048 schedTerminal::scheduler::mBuild: Set(),3049 schedTerminal::scheduler::mDone: Set(),3050 schedTerminal::scheduler::mExpect: Set(),3051 schedTerminal::scheduler::mResult: Set(),3052 schedTerminal::scheduler::mRetry: Set(),3053 schedTerminal::scheduler::mRevoke: Set(),3054 schedTerminal::scheduler::mSchedule: Set("c1"),3055 schedTerminal::scheduler::published: 0,3056 schedTerminal::scheduler::publishedBy: Set(),3057 schedTerminal::scheduler::ws:3058 Map(3059 "w1" ->3060 {3061 attached: Set(),3062 built: false,3063 expecting: false,3064 running: false,3065 session: false,3066 up: true3067 },3068 "w2" ->3069 {3070 attached: Set(),3071 built: false,3072 expecting: false,3073 running: false,3074 session: false,3075 up: true3076 }3077 )3078}30793080[State 3]3081{3082 schedTerminal::scheduler::cl: Map("c1" -> CFailed, "c2" -> CIdle),3083 schedTerminal::scheduler::crashes: 1,3084 schedTerminal::scheduler::entry: [],3085 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3086 schedTerminal::scheduler::mAssigned: Set(),3087 schedTerminal::scheduler::mBuild: Set(),3088 schedTerminal::scheduler::mDone: Set(),3089 schedTerminal::scheduler::mExpect: Set(),3090 schedTerminal::scheduler::mResult: Set(),3091 schedTerminal::scheduler::mRetry: Set(),3092 schedTerminal::scheduler::mRevoke: Set(),3093 schedTerminal::scheduler::mSchedule: Set(),3094 schedTerminal::scheduler::published: 0,3095 schedTerminal::scheduler::publishedBy: Set(),3096 schedTerminal::scheduler::ws:3097 Map(3098 "w1" ->3099 {3100 attached: Set(),3101 built: false,3102 expecting: false,3103 running: false,3104 session: false,3105 up: true3106 },3107 "w2" ->3108 {3109 attached: Set(),3110 built: false,3111 expecting: false,3112 running: false,3113 session: false,3114 up: true3115 }3116 )3117}31183119[violation] Found an issue (4741ms at 212 traces/second).3120Use --verbosity=3 to show executions.3121Use --seed=0x941f38d1898fc8c9 --backend=rust to reproduce.3122error: Invariant violated3123An example execution:31243125[State 0]3126{3127 pushFixed::push::byPath: Map(),3128 pushFixed::push::inflight: Set(),3129 pushFixed::push::left: Map(),3130 pushFixed::push::sent: Map()3131}31323133[State 1]3134{3135 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3136 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3137 pushFixed::push::left: Map(1 -> 2),3138 pushFixed::push::sent: Map(1 -> Set("a", "b"))3139}31403141[State 2]3142{3143 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3144 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3145 pushFixed::push::left: Map(1 -> 2, 2 -> 2),3146 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3147}31483149[State 3]3150{3151 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3152 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a")),3153 pushFixed::push::left: Map(1 -> 2, 2 -> 1),3154 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3155}31563157[State 4]3158{3159 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3160 pushFixed::push::inflight: Set((1, "b"), (2, "a")),3161 pushFixed::push::left: Map(1 -> 1, 2 -> 1),3162 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3163}31643165[State 5]3166{3167 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3168 pushFixed::push::inflight: Set((2, "a")),3169 pushFixed::push::left: Map(1 -> 0, 2 -> 1),3170 pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))3171}31723173[State 6]3174{3175 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3176 pushFixed::push::inflight: Set((2, "a"), (3, "a"), (3, "b")),3177 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 2),3178 pushFixed::push::sent:3179 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3180}31813182[State 7]3183{3184 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3185 pushFixed::push::inflight: Set((2, "a"), (3, "a")),3186 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1),3187 pushFixed::push::sent:3188 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3189}31903191[State 8]3192{3193 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3194 pushFixed::push::inflight: Set((2, "a")),3195 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0),3196 pushFixed::push::sent:3197 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3198}31993200[State 9]3201{3202 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3203 pushFixed::push::inflight: Set(),3204 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3205 pushFixed::push::sent:3206 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3207}32083209[ok] No violation found (4878ms at 4100 traces/second).3210Trace length statistics: max=10, min=7, average=8.083211You may increase --max-samples and --max-steps.3212Use --verbosity to produce more (or less) output.3213Use --seed=0x388faadb04ce4ff4 --backend=rust to reproduce.