nix-grpc-store-spec
checks.x86_64-linux.spec
· build #766
· 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: "w2" }],88 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),89 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),90 schedFixed::scheduler::mBuild: Set(),91 schedFixed::scheduler::mDone: Set(),92 schedFixed::scheduler::mExpect: Set("w2"),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: "w2" }],128 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),129 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),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: 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" -> CQueued),165 schedFixed::scheduler::crashes: 2,166 schedFixed::scheduler::entry:167 [{ followers: Set("c2"), leased: true, worker: "w2" }],168 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),169 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),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: false,197 up: false198 }199 )200}201202[State 5]203{204 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),205 schedFixed::scheduler::crashes: 2,206 schedFixed::scheduler::entry:207 [{ followers: Set("c2"), leased: true, worker: "w2" }],208 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),209 schedFixed::scheduler::mAssigned: Set(("c2", "w2")),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("c1"),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" -> CQueued, "c2" -> CSent("w2")),245 schedFixed::scheduler::crashes: 2,246 schedFixed::scheduler::entry:247 [{ followers: Set("c2"), leased: true, worker: "w2" }],248 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),249 schedFixed::scheduler::mAssigned: Set(),250 schedFixed::scheduler::mBuild: Set(("c2", "w2")),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("c1"),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: false,277 up: false278 }279 )280}281282[State 7]283{284 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),285 schedFixed::scheduler::crashes: 2,286 schedFixed::scheduler::entry:287 [{ followers: Set("c2"), leased: true, worker: "w2" }],288 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),289 schedFixed::scheduler::mAssigned: Set(),290 schedFixed::scheduler::mBuild: Set(("c2", "w2")),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("c1"),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: true,308 up: true309 },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("w2")),325 schedFixed::scheduler::crashes: 2,326 schedFixed::scheduler::entry:327 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],328 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),329 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),330 schedFixed::scheduler::mBuild: Set(("c2", "w2")),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: true,348 up: true349 },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("w2")),365 schedFixed::scheduler::crashes: 2,366 schedFixed::scheduler::entry:367 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],368 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),369 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),370 schedFixed::scheduler::mBuild: Set(),371 schedFixed::scheduler::mDone: Set(),372 schedFixed::scheduler::mExpect: Set(),373 schedFixed::scheduler::mResult: Set(),374 schedFixed::scheduler::mRetry: Set("c2"),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: true,388 up: true389 },390 "w2" ->391 {392 attached: Set(),393 built: false,394 expecting: false,395 running: false,396 session: false,397 up: false398 }399 )400}401402[State 10]403{404 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),405 schedFixed::scheduler::crashes: 2,406 schedFixed::scheduler::entry:407 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],408 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),409 schedFixed::scheduler::mAssigned: Set(),410 schedFixed::scheduler::mBuild: Set(("c1", "w2")),411 schedFixed::scheduler::mDone: Set(),412 schedFixed::scheduler::mExpect: Set(),413 schedFixed::scheduler::mResult: Set(),414 schedFixed::scheduler::mRetry: Set("c2"),415 schedFixed::scheduler::mRevoke: Set(),416 schedFixed::scheduler::mSchedule: Set(),417 schedFixed::scheduler::published: 0,418 schedFixed::scheduler::publishedBy: Set(),419 schedFixed::scheduler::ws:420 Map(421 "w1" ->422 {423 attached: Set(),424 built: false,425 expecting: false,426 running: false,427 session: true,428 up: true429 },430 "w2" ->431 {432 attached: Set(),433 built: false,434 expecting: false,435 running: false,436 session: false,437 up: false438 }439 )440}441442[State 11]443{444 schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),445 schedFixed::scheduler::crashes: 2,446 schedFixed::scheduler::entry:447 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],448 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),449 schedFixed::scheduler::mAssigned: Set(),450 schedFixed::scheduler::mBuild: Set(),451 schedFixed::scheduler::mDone: Set(),452 schedFixed::scheduler::mExpect: Set(),453 schedFixed::scheduler::mResult: Set(),454 schedFixed::scheduler::mRetry: Set("c1", "c2"),455 schedFixed::scheduler::mRevoke: Set(),456 schedFixed::scheduler::mSchedule: Set(),457 schedFixed::scheduler::published: 0,458 schedFixed::scheduler::publishedBy: Set(),459 schedFixed::scheduler::ws:460 Map(461 "w1" ->462 {463 attached: Set(),464 built: false,465 expecting: false,466 running: false,467 session: true,468 up: true469 },470 "w2" ->471 {472 attached: Set(),473 built: false,474 expecting: false,475 running: false,476 session: false,477 up: false478 }479 )480}481482[State 12]483{484 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),485 schedFixed::scheduler::crashes: 2,486 schedFixed::scheduler::entry:487 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],488 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),489 schedFixed::scheduler::mAssigned: Set(),490 schedFixed::scheduler::mBuild: Set(),491 schedFixed::scheduler::mDone: Set(),492 schedFixed::scheduler::mExpect: Set(),493 schedFixed::scheduler::mResult: Set(),494 schedFixed::scheduler::mRetry: Set("c2"),495 schedFixed::scheduler::mRevoke: Set(),496 schedFixed::scheduler::mSchedule: Set("c1"),497 schedFixed::scheduler::published: 0,498 schedFixed::scheduler::publishedBy: Set(),499 schedFixed::scheduler::ws:500 Map(501 "w1" ->502 {503 attached: Set(),504 built: false,505 expecting: false,506 running: false,507 session: true,508 up: true509 },510 "w2" ->511 {512 attached: Set(),513 built: false,514 expecting: false,515 running: false,516 session: false,517 up: false518 }519 )520}521522[State 13]523{524 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),525 schedFixed::scheduler::crashes: 2,526 schedFixed::scheduler::entry:527 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],528 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),529 schedFixed::scheduler::mAssigned: Set(),530 schedFixed::scheduler::mBuild: Set(),531 schedFixed::scheduler::mDone: Set(),532 schedFixed::scheduler::mExpect: Set(),533 schedFixed::scheduler::mResult: Set(),534 schedFixed::scheduler::mRetry: Set(),535 schedFixed::scheduler::mRevoke: Set(),536 schedFixed::scheduler::mSchedule: Set("c1", "c2"),537 schedFixed::scheduler::published: 0,538 schedFixed::scheduler::publishedBy: Set(),539 schedFixed::scheduler::ws:540 Map(541 "w1" ->542 {543 attached: Set(),544 built: false,545 expecting: false,546 running: false,547 session: true,548 up: true549 },550 "w2" ->551 {552 attached: Set(),553 built: false,554 expecting: false,555 running: false,556 session: false,557 up: false558 }559 )560}561562[State 14]563{564 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),565 schedFixed::scheduler::crashes: 2,566 schedFixed::scheduler::entry:567 [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],568 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),569 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),570 schedFixed::scheduler::mBuild: Set(),571 schedFixed::scheduler::mDone: Set(),572 schedFixed::scheduler::mExpect: Set(),573 schedFixed::scheduler::mResult: Set(),574 schedFixed::scheduler::mRetry: Set(),575 schedFixed::scheduler::mRevoke: Set(),576 schedFixed::scheduler::mSchedule: Set("c2"),577 schedFixed::scheduler::published: 0,578 schedFixed::scheduler::publishedBy: Set(),579 schedFixed::scheduler::ws:580 Map(581 "w1" ->582 {583 attached: Set(),584 built: false,585 expecting: false,586 running: false,587 session: true,588 up: true589 },590 "w2" ->591 {592 attached: Set(),593 built: false,594 expecting: false,595 running: false,596 session: false,597 up: false598 }599 )600}601602[State 15]603{604 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),605 schedFixed::scheduler::crashes: 2,606 schedFixed::scheduler::entry: [],607 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),608 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),609 schedFixed::scheduler::mBuild: Set(),610 schedFixed::scheduler::mDone: Set(),611 schedFixed::scheduler::mExpect: Set(),612 schedFixed::scheduler::mResult: Set(),613 schedFixed::scheduler::mRetry: Set("c1", "c2"),614 schedFixed::scheduler::mRevoke: Set(),615 schedFixed::scheduler::mSchedule: Set("c2"),616 schedFixed::scheduler::published: 0,617 schedFixed::scheduler::publishedBy: Set(),618 schedFixed::scheduler::ws:619 Map(620 "w1" ->621 {622 attached: Set(),623 built: false,624 expecting: false,625 running: false,626 session: true,627 up: true628 },629 "w2" ->630 {631 attached: Set(),632 built: false,633 expecting: false,634 running: false,635 session: false,636 up: false637 }638 )639}640641[State 16]642{643 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),644 schedFixed::scheduler::crashes: 2,645 schedFixed::scheduler::entry: [],646 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),647 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),648 schedFixed::scheduler::mBuild: Set(),649 schedFixed::scheduler::mDone: Set(),650 schedFixed::scheduler::mExpect: Set(),651 schedFixed::scheduler::mResult: Set(),652 schedFixed::scheduler::mRetry: Set("c1", "c2"),653 schedFixed::scheduler::mRevoke: Set(),654 schedFixed::scheduler::mSchedule: Set("c2"),655 schedFixed::scheduler::published: 0,656 schedFixed::scheduler::publishedBy: Set(),657 schedFixed::scheduler::ws:658 Map(659 "w1" ->660 {661 attached: Set(),662 built: false,663 expecting: false,664 running: false,665 session: true,666 up: true667 },668 "w2" ->669 {670 attached: Set(),671 built: false,672 expecting: false,673 running: false,674 session: true,675 up: true676 }677 )678}679680[State 17]681{682 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),683 schedFixed::scheduler::crashes: 2,684 schedFixed::scheduler::entry:685 [{ followers: Set("c2"), leased: true, worker: "w1" }],686 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),687 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w1")),688 schedFixed::scheduler::mBuild: Set(),689 schedFixed::scheduler::mDone: Set(),690 schedFixed::scheduler::mExpect: Set("w1"),691 schedFixed::scheduler::mResult: Set(),692 schedFixed::scheduler::mRetry: Set("c1", "c2"),693 schedFixed::scheduler::mRevoke: Set(),694 schedFixed::scheduler::mSchedule: Set(),695 schedFixed::scheduler::published: 0,696 schedFixed::scheduler::publishedBy: Set(),697 schedFixed::scheduler::ws:698 Map(699 "w1" ->700 {701 attached: Set(),702 built: false,703 expecting: false,704 running: false,705 session: true,706 up: true707 },708 "w2" ->709 {710 attached: Set(),711 built: false,712 expecting: false,713 running: false,714 session: true,715 up: true716 }717 )718}719720[State 18]721{722 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),723 schedFixed::scheduler::crashes: 2,724 schedFixed::scheduler::entry:725 [{ followers: Set("c2"), leased: true, worker: "w1" }],726 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),727 schedFixed::scheduler::mAssigned: Set(("c1", "w2")),728 schedFixed::scheduler::mBuild: Set(),729 schedFixed::scheduler::mDone: Set(),730 schedFixed::scheduler::mExpect: Set("w1"),731 schedFixed::scheduler::mResult: Set(),732 schedFixed::scheduler::mRetry: Set("c1"),733 schedFixed::scheduler::mRevoke: Set(),734 schedFixed::scheduler::mSchedule: Set("c2"),735 schedFixed::scheduler::published: 0,736 schedFixed::scheduler::publishedBy: Set(),737 schedFixed::scheduler::ws:738 Map(739 "w1" ->740 {741 attached: Set(),742 built: false,743 expecting: false,744 running: false,745 session: true,746 up: true747 },748 "w2" ->749 {750 attached: Set(),751 built: false,752 expecting: false,753 running: false,754 session: true,755 up: true756 }757 )758}759760[State 19]761{762 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),763 schedFixed::scheduler::crashes: 2,764 schedFixed::scheduler::entry:765 [{ followers: Set("c2"), leased: true, worker: "w1" }],766 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),767 schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w1")),768 schedFixed::scheduler::mBuild: Set(),769 schedFixed::scheduler::mDone: Set(),770 schedFixed::scheduler::mExpect: Set("w1"),771 schedFixed::scheduler::mResult: Set(),772 schedFixed::scheduler::mRetry: Set("c1"),773 schedFixed::scheduler::mRevoke: Set(),774 schedFixed::scheduler::mSchedule: Set(),775 schedFixed::scheduler::published: 0,776 schedFixed::scheduler::publishedBy: Set(),777 schedFixed::scheduler::ws:778 Map(779 "w1" ->780 {781 attached: Set(),782 built: false,783 expecting: false,784 running: false,785 session: true,786 up: true787 },788 "w2" ->789 {790 attached: Set(),791 built: false,792 expecting: false,793 running: false,794 session: true,795 up: true796 }797 )798}799800[State 20]801{802 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),803 schedFixed::scheduler::crashes: 2,804 schedFixed::scheduler::entry:805 [{ followers: Set("c2"), leased: true, worker: "w1" }],806 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),807 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),808 schedFixed::scheduler::mBuild: Set(),809 schedFixed::scheduler::mDone: Set(),810 schedFixed::scheduler::mExpect: Set("w1"),811 schedFixed::scheduler::mResult: Set(),812 schedFixed::scheduler::mRetry: Set(),813 schedFixed::scheduler::mRevoke: Set(),814 schedFixed::scheduler::mSchedule: Set("c1"),815 schedFixed::scheduler::published: 0,816 schedFixed::scheduler::publishedBy: Set(),817 schedFixed::scheduler::ws:818 Map(819 "w1" ->820 {821 attached: Set(),822 built: false,823 expecting: false,824 running: false,825 session: true,826 up: true827 },828 "w2" ->829 {830 attached: Set(),831 built: false,832 expecting: false,833 running: false,834 session: true,835 up: true836 }837 )838}839840[State 21]841{842 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),843 schedFixed::scheduler::crashes: 2,844 schedFixed::scheduler::entry:845 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],846 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),847 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),848 schedFixed::scheduler::mBuild: Set(),849 schedFixed::scheduler::mDone: Set(),850 schedFixed::scheduler::mExpect: Set("w1"),851 schedFixed::scheduler::mResult: Set(),852 schedFixed::scheduler::mRetry: Set(),853 schedFixed::scheduler::mRevoke: Set(),854 schedFixed::scheduler::mSchedule: Set(),855 schedFixed::scheduler::published: 0,856 schedFixed::scheduler::publishedBy: Set(),857 schedFixed::scheduler::ws:858 Map(859 "w1" ->860 {861 attached: Set(),862 built: false,863 expecting: false,864 running: false,865 session: true,866 up: true867 },868 "w2" ->869 {870 attached: Set(),871 built: false,872 expecting: false,873 running: false,874 session: true,875 up: true876 }877 )878}879880[State 22]881{882 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),883 schedFixed::scheduler::crashes: 2,884 schedFixed::scheduler::entry:885 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],886 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),887 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),888 schedFixed::scheduler::mBuild: Set(("c1", "w1")),889 schedFixed::scheduler::mDone: Set(),890 schedFixed::scheduler::mExpect: Set("w1"),891 schedFixed::scheduler::mResult: Set(),892 schedFixed::scheduler::mRetry: Set(),893 schedFixed::scheduler::mRevoke: Set(),894 schedFixed::scheduler::mSchedule: Set(),895 schedFixed::scheduler::published: 0,896 schedFixed::scheduler::publishedBy: Set(),897 schedFixed::scheduler::ws:898 Map(899 "w1" ->900 {901 attached: Set(),902 built: false,903 expecting: false,904 running: false,905 session: true,906 up: true907 },908 "w2" ->909 {910 attached: Set(),911 built: false,912 expecting: false,913 running: false,914 session: true,915 up: true916 }917 )918}919920[State 23]921{922 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),923 schedFixed::scheduler::crashes: 2,924 schedFixed::scheduler::entry:925 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],926 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),927 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),928 schedFixed::scheduler::mBuild: Set(("c1", "w1")),929 schedFixed::scheduler::mDone: Set(),930 schedFixed::scheduler::mExpect: Set(),931 schedFixed::scheduler::mResult: Set(),932 schedFixed::scheduler::mRetry: Set(),933 schedFixed::scheduler::mRevoke: Set(),934 schedFixed::scheduler::mSchedule: Set(),935 schedFixed::scheduler::published: 0,936 schedFixed::scheduler::publishedBy: Set(),937 schedFixed::scheduler::ws:938 Map(939 "w1" ->940 {941 attached: Set(),942 built: false,943 expecting: true,944 running: true,945 session: true,946 up: true947 },948 "w2" ->949 {950 attached: Set(),951 built: false,952 expecting: false,953 running: false,954 session: true,955 up: true956 }957 )958}959960[State 24]961{962 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),963 schedFixed::scheduler::crashes: 2,964 schedFixed::scheduler::entry:965 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],966 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),967 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),968 schedFixed::scheduler::mBuild: Set(("c1", "w1")),969 schedFixed::scheduler::mDone: Set("w1"),970 schedFixed::scheduler::mExpect: Set(),971 schedFixed::scheduler::mResult: Set(),972 schedFixed::scheduler::mRetry: Set(),973 schedFixed::scheduler::mRevoke: Set(),974 schedFixed::scheduler::mSchedule: Set(),975 schedFixed::scheduler::published: 1,976 schedFixed::scheduler::publishedBy: Set("w1"),977 schedFixed::scheduler::ws:978 Map(979 "w1" ->980 {981 attached: Set(),982 built: true,983 expecting: false,984 running: false,985 session: true,986 up: true987 },988 "w2" ->989 {990 attached: Set(),991 built: false,992 expecting: false,993 running: false,994 session: true,995 up: true996 }997 )998}9991000[State 25]1001{1002 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),1003 schedFixed::scheduler::crashes: 2,1004 schedFixed::scheduler::entry:1005 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1006 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1007 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1008 schedFixed::scheduler::mBuild: Set(),1009 schedFixed::scheduler::mDone: Set("w1"),1010 schedFixed::scheduler::mExpect: Set(),1011 schedFixed::scheduler::mResult: Set("c1"),1012 schedFixed::scheduler::mRetry: Set(),1013 schedFixed::scheduler::mRevoke: Set(),1014 schedFixed::scheduler::mSchedule: Set(),1015 schedFixed::scheduler::published: 1,1016 schedFixed::scheduler::publishedBy: Set("w1"),1017 schedFixed::scheduler::ws:1018 Map(1019 "w1" ->1020 {1021 attached: Set(),1022 built: true,1023 expecting: false,1024 running: false,1025 session: true,1026 up: true1027 },1028 "w2" ->1029 {1030 attached: Set(),1031 built: false,1032 expecting: false,1033 running: false,1034 session: true,1035 up: true1036 }1037 )1038}10391040[State 26]1041{1042 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),1043 schedFixed::scheduler::crashes: 2,1044 schedFixed::scheduler::entry: [],1045 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1046 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1047 schedFixed::scheduler::mBuild: Set(),1048 schedFixed::scheduler::mDone: Set(),1049 schedFixed::scheduler::mExpect: Set(),1050 schedFixed::scheduler::mResult: Set("c1"),1051 schedFixed::scheduler::mRetry: Set(),1052 schedFixed::scheduler::mRevoke: Set(),1053 schedFixed::scheduler::mSchedule: Set(),1054 schedFixed::scheduler::published: 1,1055 schedFixed::scheduler::publishedBy: Set("w1"),1056 schedFixed::scheduler::ws:1057 Map(1058 "w1" ->1059 {1060 attached: Set(),1061 built: true,1062 expecting: false,1063 running: false,1064 session: true,1065 up: true1066 },1067 "w2" ->1068 {1069 attached: Set(),1070 built: false,1071 expecting: false,1072 running: false,1073 session: true,1074 up: true1075 }1076 )1077}10781079[State 27]1080{1081 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CQueued),1082 schedFixed::scheduler::crashes: 2,1083 schedFixed::scheduler::entry: [],1084 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1085 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),1086 schedFixed::scheduler::mBuild: Set(),1087 schedFixed::scheduler::mDone: Set(),1088 schedFixed::scheduler::mExpect: Set(),1089 schedFixed::scheduler::mResult: Set(),1090 schedFixed::scheduler::mRetry: Set(),1091 schedFixed::scheduler::mRevoke: Set(),1092 schedFixed::scheduler::mSchedule: Set(),1093 schedFixed::scheduler::published: 1,1094 schedFixed::scheduler::publishedBy: Set("w1"),1095 schedFixed::scheduler::ws:1096 Map(1097 "w1" ->1098 {1099 attached: Set(),1100 built: true,1101 expecting: false,1102 running: false,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" -> CDone, "c2" -> CSent("w1")),1121 schedFixed::scheduler::crashes: 2,1122 schedFixed::scheduler::entry: [],1123 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1124 schedFixed::scheduler::mAssigned: Set(),1125 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1126 schedFixed::scheduler::mDone: Set(),1127 schedFixed::scheduler::mExpect: Set(),1128 schedFixed::scheduler::mResult: Set(),1129 schedFixed::scheduler::mRetry: Set(),1130 schedFixed::scheduler::mRevoke: Set(),1131 schedFixed::scheduler::mSchedule: Set(),1132 schedFixed::scheduler::published: 1,1133 schedFixed::scheduler::publishedBy: Set("w1"),1134 schedFixed::scheduler::ws:1135 Map(1136 "w1" ->1137 {1138 attached: Set(),1139 built: true,1140 expecting: false,1141 running: false,1142 session: true,1143 up: true1144 },1145 "w2" ->1146 {1147 attached: Set(),1148 built: false,1149 expecting: false,1150 running: false,1151 session: true,1152 up: true1153 }1154 )1155}11561157[State 29]1158{1159 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w1")),1160 schedFixed::scheduler::crashes: 2,1161 schedFixed::scheduler::entry: [],1162 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1163 schedFixed::scheduler::mAssigned: Set(),1164 schedFixed::scheduler::mBuild: Set(),1165 schedFixed::scheduler::mDone: Set(),1166 schedFixed::scheduler::mExpect: Set(),1167 schedFixed::scheduler::mResult: Set("c2"),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("w1"),1173 schedFixed::scheduler::ws:1174 Map(1175 "w1" ->1176 {1177 attached: Set(),1178 built: true,1179 expecting: false,1180 running: false,1181 session: true,1182 up: true1183 },1184 "w2" ->1185 {1186 attached: Set(),1187 built: false,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(),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("w1"),1212 schedFixed::scheduler::ws:1213 Map(1214 "w1" ->1215 {1216 attached: Set(),1217 built: true,1218 expecting: false,1219 running: false,1220 session: true,1221 up: true1222 },1223 "w2" ->1224 {1225 attached: Set(),1226 built: false,1227 expecting: false,1228 running: false,1229 session: true,1230 up: true1231 }1232 )1233}12341235[ok] No violation found (457ms at 65646 traces/second).1236Trace length statistics: max=30, min=16, average=18.971237You may increase --max-samples and --max-steps.1238Use --verbosity to produce more (or less) output.1239Use --seed=0x56c3b4f5101b5437 --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" -> CQueued, "c2" -> CIdle),1284 schedNoRevoke::scheduler::crashes: 0,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("c1"),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: true,1306 up: true1307 },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: 0,1324 schedNoRevoke::scheduler::entry:1325 [{ followers: Set("c1"), leased: true, worker: "w2" }],1326 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1327 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1328 schedNoRevoke::scheduler::mBuild: Set(),1329 schedNoRevoke::scheduler::mDone: Set(),1330 schedNoRevoke::scheduler::mExpect: Set("w2"),1331 schedNoRevoke::scheduler::mResult: Set(),1332 schedNoRevoke::scheduler::mRetry: Set(),1333 schedNoRevoke::scheduler::mRevoke: Set(),1334 schedNoRevoke::scheduler::mSchedule: Set(),1335 schedNoRevoke::scheduler::published: 0,1336 schedNoRevoke::scheduler::publishedBy: Set(),1337 schedNoRevoke::scheduler::ws:1338 Map(1339 "w1" ->1340 {1341 attached: Set(),1342 built: false,1343 expecting: false,1344 running: false,1345 session: true,1346 up: true1347 },1348 "w2" ->1349 {1350 attached: Set(),1351 built: false,1352 expecting: false,1353 running: false,1354 session: true,1355 up: true1356 }1357 )1358}13591360[State 3]1361{1362 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1363 schedNoRevoke::scheduler::crashes: 1,1364 schedNoRevoke::scheduler::entry:1365 [{ followers: Set("c1"), leased: true, worker: "w2" }],1366 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1367 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1368 schedNoRevoke::scheduler::mBuild: Set(),1369 schedNoRevoke::scheduler::mDone: Set(),1370 schedNoRevoke::scheduler::mExpect: Set("w2"),1371 schedNoRevoke::scheduler::mResult: Set(),1372 schedNoRevoke::scheduler::mRetry: Set(),1373 schedNoRevoke::scheduler::mRevoke: Set(),1374 schedNoRevoke::scheduler::mSchedule: Set(),1375 schedNoRevoke::scheduler::published: 0,1376 schedNoRevoke::scheduler::publishedBy: Set(),1377 schedNoRevoke::scheduler::ws:1378 Map(1379 "w1" ->1380 {1381 attached: Set(),1382 built: false,1383 expecting: false,1384 running: false,1385 session: false,1386 up: false1387 },1388 "w2" ->1389 {1390 attached: Set(),1391 built: false,1392 expecting: false,1393 running: false,1394 session: true,1395 up: true1396 }1397 )1398}13991400[State 4]1401{1402 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1403 schedNoRevoke::scheduler::crashes: 1,1404 schedNoRevoke::scheduler::entry:1405 [{ followers: Set("c1"), leased: true, worker: "w2" }],1406 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1407 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1408 schedNoRevoke::scheduler::mBuild: Set(),1409 schedNoRevoke::scheduler::mDone: Set(),1410 schedNoRevoke::scheduler::mExpect: Set(),1411 schedNoRevoke::scheduler::mResult: Set(),1412 schedNoRevoke::scheduler::mRetry: Set(),1413 schedNoRevoke::scheduler::mRevoke: Set(),1414 schedNoRevoke::scheduler::mSchedule: Set(),1415 schedNoRevoke::scheduler::published: 0,1416 schedNoRevoke::scheduler::publishedBy: Set(),1417 schedNoRevoke::scheduler::ws:1418 Map(1419 "w1" ->1420 {1421 attached: Set(),1422 built: false,1423 expecting: false,1424 running: false,1425 session: false,1426 up: false1427 },1428 "w2" ->1429 {1430 attached: Set(),1431 built: false,1432 expecting: true,1433 running: true,1434 session: true,1435 up: true1436 }1437 )1438}14391440[State 5]1441{1442 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1443 schedNoRevoke::scheduler::crashes: 2,1444 schedNoRevoke::scheduler::entry: [],1445 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1446 schedNoRevoke::scheduler::mAssigned: Set(),1447 schedNoRevoke::scheduler::mBuild: Set(),1448 schedNoRevoke::scheduler::mDone: Set(),1449 schedNoRevoke::scheduler::mExpect: Set(),1450 schedNoRevoke::scheduler::mResult: Set(),1451 schedNoRevoke::scheduler::mRetry: Set("c1"),1452 schedNoRevoke::scheduler::mRevoke: Set(),1453 schedNoRevoke::scheduler::mSchedule: Set(),1454 schedNoRevoke::scheduler::published: 0,1455 schedNoRevoke::scheduler::publishedBy: Set(),1456 schedNoRevoke::scheduler::ws:1457 Map(1458 "w1" ->1459 {1460 attached: Set(),1461 built: false,1462 expecting: false,1463 running: false,1464 session: false,1465 up: false1466 },1467 "w2" ->1468 {1469 attached: Set(),1470 built: false,1471 expecting: true,1472 running: true,1473 session: false,1474 up: true1475 }1476 )1477}14781479[State 6]1480{1481 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1482 schedNoRevoke::scheduler::crashes: 2,1483 schedNoRevoke::scheduler::entry: [],1484 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1485 schedNoRevoke::scheduler::mAssigned: Set(),1486 schedNoRevoke::scheduler::mBuild: Set(),1487 schedNoRevoke::scheduler::mDone: Set(),1488 schedNoRevoke::scheduler::mExpect: Set(),1489 schedNoRevoke::scheduler::mResult: Set(),1490 schedNoRevoke::scheduler::mRetry: Set("c1"),1491 schedNoRevoke::scheduler::mRevoke: Set(),1492 schedNoRevoke::scheduler::mSchedule: Set("c2"),1493 schedNoRevoke::scheduler::published: 0,1494 schedNoRevoke::scheduler::publishedBy: Set(),1495 schedNoRevoke::scheduler::ws:1496 Map(1497 "w1" ->1498 {1499 attached: Set(),1500 built: false,1501 expecting: false,1502 running: false,1503 session: false,1504 up: false1505 },1506 "w2" ->1507 {1508 attached: Set(),1509 built: false,1510 expecting: true,1511 running: true,1512 session: false,1513 up: true1514 }1515 )1516}15171518[State 7]1519{1520 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1521 schedNoRevoke::scheduler::crashes: 2,1522 schedNoRevoke::scheduler::entry: [],1523 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1524 schedNoRevoke::scheduler::mAssigned: Set(),1525 schedNoRevoke::scheduler::mBuild: Set(),1526 schedNoRevoke::scheduler::mDone: Set(),1527 schedNoRevoke::scheduler::mExpect: Set(),1528 schedNoRevoke::scheduler::mResult: Set(),1529 schedNoRevoke::scheduler::mRetry: Set("c1"),1530 schedNoRevoke::scheduler::mRevoke: Set(),1531 schedNoRevoke::scheduler::mSchedule: Set("c2"),1532 schedNoRevoke::scheduler::published: 0,1533 schedNoRevoke::scheduler::publishedBy: Set(),1534 schedNoRevoke::scheduler::ws:1535 Map(1536 "w1" ->1537 {1538 attached: Set(),1539 built: false,1540 expecting: false,1541 running: false,1542 session: true,1543 up: true1544 },1545 "w2" ->1546 {1547 attached: Set(),1548 built: false,1549 expecting: true,1550 running: true,1551 session: false,1552 up: true1553 }1554 )1555}15561557[State 8]1558{1559 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1560 schedNoRevoke::scheduler::crashes: 2,1561 schedNoRevoke::scheduler::entry:1562 [{ followers: Set("c2"), leased: true, worker: "w1" }],1563 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1564 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1565 schedNoRevoke::scheduler::mBuild: Set(),1566 schedNoRevoke::scheduler::mDone: Set(),1567 schedNoRevoke::scheduler::mExpect: Set("w1"),1568 schedNoRevoke::scheduler::mResult: Set(),1569 schedNoRevoke::scheduler::mRetry: Set("c1"),1570 schedNoRevoke::scheduler::mRevoke: Set(),1571 schedNoRevoke::scheduler::mSchedule: Set(),1572 schedNoRevoke::scheduler::published: 0,1573 schedNoRevoke::scheduler::publishedBy: Set(),1574 schedNoRevoke::scheduler::ws:1575 Map(1576 "w1" ->1577 {1578 attached: Set(),1579 built: false,1580 expecting: false,1581 running: false,1582 session: true,1583 up: true1584 },1585 "w2" ->1586 {1587 attached: Set(),1588 built: false,1589 expecting: true,1590 running: true,1591 session: false,1592 up: true1593 }1594 )1595}15961597[State 9]1598{1599 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1600 schedNoRevoke::scheduler::crashes: 2,1601 schedNoRevoke::scheduler::entry:1602 [{ followers: Set("c2"), leased: true, worker: "w1" }],1603 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1604 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1605 schedNoRevoke::scheduler::mBuild: Set(),1606 schedNoRevoke::scheduler::mDone: Set(),1607 schedNoRevoke::scheduler::mExpect: Set(),1608 schedNoRevoke::scheduler::mResult: Set(),1609 schedNoRevoke::scheduler::mRetry: Set("c1"),1610 schedNoRevoke::scheduler::mRevoke: Set(),1611 schedNoRevoke::scheduler::mSchedule: Set(),1612 schedNoRevoke::scheduler::published: 0,1613 schedNoRevoke::scheduler::publishedBy: Set(),1614 schedNoRevoke::scheduler::ws:1615 Map(1616 "w1" ->1617 {1618 attached: Set(),1619 built: false,1620 expecting: true,1621 running: true,1622 session: true,1623 up: true1624 },1625 "w2" ->1626 {1627 attached: Set(),1628 built: false,1629 expecting: true,1630 running: true,1631 session: false,1632 up: true1633 }1634 )1635}16361637[State 10]1638{1639 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1640 schedNoRevoke::scheduler::crashes: 2,1641 schedNoRevoke::scheduler::entry:1642 [{ followers: Set("c2"), leased: true, worker: "w1" }],1643 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1644 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1645 schedNoRevoke::scheduler::mBuild: Set(),1646 schedNoRevoke::scheduler::mDone: Set(),1647 schedNoRevoke::scheduler::mExpect: Set(),1648 schedNoRevoke::scheduler::mResult: Set(),1649 schedNoRevoke::scheduler::mRetry: Set("c1"),1650 schedNoRevoke::scheduler::mRevoke: Set(),1651 schedNoRevoke::scheduler::mSchedule: Set(),1652 schedNoRevoke::scheduler::published: 0,1653 schedNoRevoke::scheduler::publishedBy: Set(),1654 schedNoRevoke::scheduler::ws:1655 Map(1656 "w1" ->1657 {1658 attached: Set(),1659 built: false,1660 expecting: true,1661 running: true,1662 session: true,1663 up: true1664 },1665 "w2" ->1666 {1667 attached: Set(),1668 built: false,1669 expecting: true,1670 running: true,1671 session: true,1672 up: true1673 }1674 )1675}16761677[violation] Found an issue (497ms at 58316 traces/second).1678Use --verbosity=3 to show executions.1679Use --seed=0x41125521059f6659 --backend=rust to reproduce.1680error: Invariant violated1681An example execution:16821683[State 0]1684{1685 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1686 schedNoFence::scheduler::crashes: 0,1687 schedNoFence::scheduler::entry: [],1688 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1689 schedNoFence::scheduler::mAssigned: Set(),1690 schedNoFence::scheduler::mBuild: Set(),1691 schedNoFence::scheduler::mDone: Set(),1692 schedNoFence::scheduler::mExpect: Set(),1693 schedNoFence::scheduler::mResult: Set(),1694 schedNoFence::scheduler::mRetry: Set(),1695 schedNoFence::scheduler::mRevoke: Set(),1696 schedNoFence::scheduler::mSchedule: Set(),1697 schedNoFence::scheduler::published: 0,1698 schedNoFence::scheduler::publishedBy: Set(),1699 schedNoFence::scheduler::ws:1700 Map(1701 "w1" ->1702 {1703 attached: Set(),1704 built: false,1705 expecting: false,1706 running: false,1707 session: true,1708 up: true1709 },1710 "w2" ->1711 {1712 attached: Set(),1713 built: false,1714 expecting: false,1715 running: false,1716 session: true,1717 up: true1718 }1719 )1720}17211722[State 1]1723{1724 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1725 schedNoFence::scheduler::crashes: 0,1726 schedNoFence::scheduler::entry: [],1727 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1728 schedNoFence::scheduler::mAssigned: Set(),1729 schedNoFence::scheduler::mBuild: Set(),1730 schedNoFence::scheduler::mDone: Set(),1731 schedNoFence::scheduler::mExpect: Set(),1732 schedNoFence::scheduler::mResult: Set(),1733 schedNoFence::scheduler::mRetry: Set(),1734 schedNoFence::scheduler::mRevoke: Set(),1735 schedNoFence::scheduler::mSchedule: Set("c2"),1736 schedNoFence::scheduler::published: 0,1737 schedNoFence::scheduler::publishedBy: Set(),1738 schedNoFence::scheduler::ws:1739 Map(1740 "w1" ->1741 {1742 attached: Set(),1743 built: false,1744 expecting: false,1745 running: false,1746 session: true,1747 up: true1748 },1749 "w2" ->1750 {1751 attached: Set(),1752 built: false,1753 expecting: false,1754 running: false,1755 session: true,1756 up: true1757 }1758 )1759}17601761[State 2]1762{1763 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1764 schedNoFence::scheduler::crashes: 0,1765 schedNoFence::scheduler::entry:1766 [{ followers: Set("c2"), leased: true, worker: "w1" }],1767 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1768 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1769 schedNoFence::scheduler::mBuild: Set(),1770 schedNoFence::scheduler::mDone: Set(),1771 schedNoFence::scheduler::mExpect: Set("w1"),1772 schedNoFence::scheduler::mResult: Set(),1773 schedNoFence::scheduler::mRetry: Set(),1774 schedNoFence::scheduler::mRevoke: Set(),1775 schedNoFence::scheduler::mSchedule: Set(),1776 schedNoFence::scheduler::published: 0,1777 schedNoFence::scheduler::publishedBy: Set(),1778 schedNoFence::scheduler::ws:1779 Map(1780 "w1" ->1781 {1782 attached: Set(),1783 built: false,1784 expecting: false,1785 running: false,1786 session: true,1787 up: true1788 },1789 "w2" ->1790 {1791 attached: Set(),1792 built: false,1793 expecting: false,1794 running: false,1795 session: true,1796 up: true1797 }1798 )1799}18001801[State 3]1802{1803 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1804 schedNoFence::scheduler::crashes: 0,1805 schedNoFence::scheduler::entry:1806 [{ followers: Set("c2"), leased: true, worker: "w1" }],1807 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1808 schedNoFence::scheduler::mAssigned: Set(("c2", "w1")),1809 schedNoFence::scheduler::mBuild: Set(),1810 schedNoFence::scheduler::mDone: Set(),1811 schedNoFence::scheduler::mExpect: Set(),1812 schedNoFence::scheduler::mResult: Set(),1813 schedNoFence::scheduler::mRetry: Set(),1814 schedNoFence::scheduler::mRevoke: Set(),1815 schedNoFence::scheduler::mSchedule: Set(),1816 schedNoFence::scheduler::published: 0,1817 schedNoFence::scheduler::publishedBy: Set(),1818 schedNoFence::scheduler::ws:1819 Map(1820 "w1" ->1821 {1822 attached: Set(),1823 built: false,1824 expecting: true,1825 running: true,1826 session: true,1827 up: true1828 },1829 "w2" ->1830 {1831 attached: Set(),1832 built: false,1833 expecting: false,1834 running: false,1835 session: true,1836 up: true1837 }1838 )1839}18401841[State 4]1842{1843 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1844 schedNoFence::scheduler::crashes: 1,1845 schedNoFence::scheduler::entry: [],1846 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1847 schedNoFence::scheduler::mAssigned: Set(),1848 schedNoFence::scheduler::mBuild: Set(),1849 schedNoFence::scheduler::mDone: Set(),1850 schedNoFence::scheduler::mExpect: Set(),1851 schedNoFence::scheduler::mResult: Set(),1852 schedNoFence::scheduler::mRetry: Set("c2"),1853 schedNoFence::scheduler::mRevoke: Set(),1854 schedNoFence::scheduler::mSchedule: Set(),1855 schedNoFence::scheduler::published: 0,1856 schedNoFence::scheduler::publishedBy: Set(),1857 schedNoFence::scheduler::ws:1858 Map(1859 "w1" ->1860 {1861 attached: Set(),1862 built: false,1863 expecting: true,1864 running: true,1865 session: false,1866 up: true1867 },1868 "w2" ->1869 {1870 attached: Set(),1871 built: false,1872 expecting: false,1873 running: false,1874 session: false,1875 up: true1876 }1877 )1878}18791880[State 5]1881{1882 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1883 schedNoFence::scheduler::crashes: 2,1884 schedNoFence::scheduler::entry: [],1885 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1886 schedNoFence::scheduler::mAssigned: Set(),1887 schedNoFence::scheduler::mBuild: Set(),1888 schedNoFence::scheduler::mDone: Set(),1889 schedNoFence::scheduler::mExpect: Set(),1890 schedNoFence::scheduler::mResult: Set(),1891 schedNoFence::scheduler::mRetry: Set("c2"),1892 schedNoFence::scheduler::mRevoke: Set(),1893 schedNoFence::scheduler::mSchedule: Set(),1894 schedNoFence::scheduler::published: 0,1895 schedNoFence::scheduler::publishedBy: Set(),1896 schedNoFence::scheduler::ws:1897 Map(1898 "w1" ->1899 {1900 attached: Set(),1901 built: false,1902 expecting: true,1903 running: true,1904 session: false,1905 up: true1906 },1907 "w2" ->1908 {1909 attached: Set(),1910 built: false,1911 expecting: false,1912 running: false,1913 session: false,1914 up: true1915 }1916 )1917}19181919[State 6]1920{1921 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),1922 schedNoFence::scheduler::crashes: 2,1923 schedNoFence::scheduler::entry: [],1924 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1925 schedNoFence::scheduler::mAssigned: Set(),1926 schedNoFence::scheduler::mBuild: Set(),1927 schedNoFence::scheduler::mDone: Set(),1928 schedNoFence::scheduler::mExpect: Set(),1929 schedNoFence::scheduler::mResult: Set(),1930 schedNoFence::scheduler::mRetry: Set("c2"),1931 schedNoFence::scheduler::mRevoke: Set(),1932 schedNoFence::scheduler::mSchedule: Set(),1933 schedNoFence::scheduler::published: 0,1934 schedNoFence::scheduler::publishedBy: Set(),1935 schedNoFence::scheduler::ws:1936 Map(1937 "w1" ->1938 {1939 attached: Set(),1940 built: false,1941 expecting: true,1942 running: true,1943 session: false,1944 up: true1945 },1946 "w2" ->1947 {1948 attached: Set(),1949 built: false,1950 expecting: false,1951 running: false,1952 session: true,1953 up: true1954 }1955 )1956}19571958[State 7]1959{1960 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "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(),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: true,1981 running: true,1982 session: false,1983 up: true1984 },1985 "w2" ->1986 {1987 attached: Set(),1988 built: false,1989 expecting: false,1990 running: false,1991 session: true,1992 up: true1993 }1994 )1995}19961997[State 8]1998{1999 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2000 schedNoFence::scheduler::crashes: 2,2001 schedNoFence::scheduler::entry: [],2002 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(),2009 schedNoFence::scheduler::mRevoke: Set(),2010 schedNoFence::scheduler::mSchedule: Set("c1", "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: true,2020 running: true,2021 session: false,2022 up: true2023 },2024 "w2" ->2025 {2026 attached: Set(),2027 built: false,2028 expecting: false,2029 running: false,2030 session: true,2031 up: true2032 }2033 )2034}20352036[State 9]2037{2038 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2039 schedNoFence::scheduler::crashes: 2,2040 schedNoFence::scheduler::entry:2041 [{ followers: Set("c1"), leased: true, worker: "w2" }],2042 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2043 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2044 schedNoFence::scheduler::mBuild: Set(),2045 schedNoFence::scheduler::mDone: Set(),2046 schedNoFence::scheduler::mExpect: Set("w2"),2047 schedNoFence::scheduler::mResult: Set(),2048 schedNoFence::scheduler::mRetry: Set(),2049 schedNoFence::scheduler::mRevoke: Set(),2050 schedNoFence::scheduler::mSchedule: Set("c2"),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: true,2060 running: true,2061 session: false,2062 up: true2063 },2064 "w2" ->2065 {2066 attached: Set(),2067 built: false,2068 expecting: false,2069 running: false,2070 session: true,2071 up: true2072 }2073 )2074}20752076[State 10]2077{2078 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2079 schedNoFence::scheduler::crashes: 2,2080 schedNoFence::scheduler::entry:2081 [{ followers: Set("c1"), leased: true, worker: "w2" }],2082 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2083 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2084 schedNoFence::scheduler::mBuild: Set(),2085 schedNoFence::scheduler::mDone: Set(),2086 schedNoFence::scheduler::mExpect: Set(),2087 schedNoFence::scheduler::mResult: Set(),2088 schedNoFence::scheduler::mRetry: Set(),2089 schedNoFence::scheduler::mRevoke: Set(),2090 schedNoFence::scheduler::mSchedule: Set("c2"),2091 schedNoFence::scheduler::published: 0,2092 schedNoFence::scheduler::publishedBy: Set(),2093 schedNoFence::scheduler::ws:2094 Map(2095 "w1" ->2096 {2097 attached: Set(),2098 built: false,2099 expecting: true,2100 running: true,2101 session: false,2102 up: true2103 },2104 "w2" ->2105 {2106 attached: Set(),2107 built: false,2108 expecting: true,2109 running: true,2110 session: true,2111 up: true2112 }2113 )2114}21152116[State 11]2117{2118 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2119 schedNoFence::scheduler::crashes: 2,2120 schedNoFence::scheduler::entry:2121 [{ followers: Set("c1"), leased: true, worker: "w2" }],2122 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2123 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),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(),2129 schedNoFence::scheduler::mRevoke: Set(),2130 schedNoFence::scheduler::mSchedule: Set("c2"),2131 schedNoFence::scheduler::published: 1,2132 schedNoFence::scheduler::publishedBy: Set("w1"),2133 schedNoFence::scheduler::ws:2134 Map(2135 "w1" ->2136 {2137 attached: Set(),2138 built: true,2139 expecting: false,2140 running: false,2141 session: false,2142 up: true2143 },2144 "w2" ->2145 {2146 attached: Set(),2147 built: false,2148 expecting: true,2149 running: true,2150 session: true,2151 up: true2152 }2153 )2154}21552156[State 12]2157{2158 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2159 schedNoFence::scheduler::crashes: 2,2160 schedNoFence::scheduler::entry:2161 [{ followers: Set("c1"), leased: true, worker: "w2" }],2162 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2163 schedNoFence::scheduler::mAssigned: Set(("c1", "w2")),2164 schedNoFence::scheduler::mBuild: Set(),2165 schedNoFence::scheduler::mDone: Set("w2"),2166 schedNoFence::scheduler::mExpect: Set(),2167 schedNoFence::scheduler::mResult: Set(),2168 schedNoFence::scheduler::mRetry: Set(),2169 schedNoFence::scheduler::mRevoke: Set(),2170 schedNoFence::scheduler::mSchedule: Set("c2"),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: false,2182 up: true2183 },2184 "w2" ->2185 {2186 attached: Set(),2187 built: true,2188 expecting: false,2189 running: false,2190 session: true,2191 up: true2192 }2193 )2194}21952196[violation] Found an issue (461ms at 59959 traces/second).2197Use --verbosity=3 to show executions.2198Use --seed=0xdeadd562ccd8380c --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" -> CIdle, "c2" -> CQueued),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("c2"),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" -> CIdle, "c2" -> CQueued),2283 schedNoPush::scheduler::crashes: 0,2284 schedNoPush::scheduler::entry:2285 [{ followers: Set("c2"), leased: true, worker: "w2" }],2286 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2287 schedNoPush::scheduler::mAssigned: Set(("c2", "w2")),2288 schedNoPush::scheduler::mBuild: Set(),2289 schedNoPush::scheduler::mDone: Set(),2290 schedNoPush::scheduler::mExpect: Set(),2291 schedNoPush::scheduler::mResult: Set(),2292 schedNoPush::scheduler::mRetry: Set(),2293 schedNoPush::scheduler::mRevoke: Set(),2294 schedNoPush::scheduler::mSchedule: Set(),2295 schedNoPush::scheduler::published: 0,2296 schedNoPush::scheduler::publishedBy: Set(),2297 schedNoPush::scheduler::ws:2298 Map(2299 "w1" ->2300 {2301 attached: Set(),2302 built: false,2303 expecting: false,2304 running: false,2305 session: true,2306 up: true2307 },2308 "w2" ->2309 {2310 attached: Set(),2311 built: false,2312 expecting: false,2313 running: false,2314 session: true,2315 up: true2316 }2317 )2318}23192320[State 3]2321{2322 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2323 schedNoPush::scheduler::crashes: 0,2324 schedNoPush::scheduler::entry:2325 [{ followers: Set("c2"), leased: true, worker: "w2" }],2326 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2327 schedNoPush::scheduler::mAssigned: Set(),2328 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2329 schedNoPush::scheduler::mDone: Set(),2330 schedNoPush::scheduler::mExpect: Set(),2331 schedNoPush::scheduler::mResult: Set(),2332 schedNoPush::scheduler::mRetry: Set(),2333 schedNoPush::scheduler::mRevoke: Set(),2334 schedNoPush::scheduler::mSchedule: Set(),2335 schedNoPush::scheduler::published: 0,2336 schedNoPush::scheduler::publishedBy: Set(),2337 schedNoPush::scheduler::ws:2338 Map(2339 "w1" ->2340 {2341 attached: Set(),2342 built: false,2343 expecting: false,2344 running: false,2345 session: true,2346 up: true2347 },2348 "w2" ->2349 {2350 attached: Set(),2351 built: false,2352 expecting: false,2353 running: false,2354 session: true,2355 up: true2356 }2357 )2358}23592360[State 4]2361{2362 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2363 schedNoPush::scheduler::crashes: 1,2364 schedNoPush::scheduler::entry: [],2365 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2366 schedNoPush::scheduler::mAssigned: Set(),2367 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),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: true2386 },2387 "w2" ->2388 {2389 attached: Set(),2390 built: false,2391 expecting: false,2392 running: false,2393 session: false,2394 up: true2395 }2396 )2397}23982399[State 5]2400{2401 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2402 schedNoPush::scheduler::crashes: 1,2403 schedNoPush::scheduler::entry: [],2404 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2405 schedNoPush::scheduler::mAssigned: Set(),2406 schedNoPush::scheduler::mBuild: Set(("c2", "w2")),2407 schedNoPush::scheduler::mDone: Set(),2408 schedNoPush::scheduler::mExpect: Set(),2409 schedNoPush::scheduler::mResult: Set(),2410 schedNoPush::scheduler::mRetry: Set(),2411 schedNoPush::scheduler::mRevoke: Set(),2412 schedNoPush::scheduler::mSchedule: Set(),2413 schedNoPush::scheduler::published: 0,2414 schedNoPush::scheduler::publishedBy: Set(),2415 schedNoPush::scheduler::ws:2416 Map(2417 "w1" ->2418 {2419 attached: Set(),2420 built: false,2421 expecting: false,2422 running: false,2423 session: false,2424 up: true2425 },2426 "w2" ->2427 {2428 attached: Set(),2429 built: false,2430 expecting: false,2431 running: false,2432 session: true,2433 up: true2434 }2435 )2436}24372438[State 6]2439{2440 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w2")),2441 schedNoPush::scheduler::crashes: 1,2442 schedNoPush::scheduler::entry: [],2443 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2444 schedNoPush::scheduler::mAssigned: Set(),2445 schedNoPush::scheduler::mBuild: Set(),2446 schedNoPush::scheduler::mDone: Set(),2447 schedNoPush::scheduler::mExpect: Set(),2448 schedNoPush::scheduler::mResult: Set(),2449 schedNoPush::scheduler::mRetry: Set(),2450 schedNoPush::scheduler::mRevoke: Set(),2451 schedNoPush::scheduler::mSchedule: Set(),2452 schedNoPush::scheduler::published: 0,2453 schedNoPush::scheduler::publishedBy: Set(),2454 schedNoPush::scheduler::ws:2455 Map(2456 "w1" ->2457 {2458 attached: Set(),2459 built: false,2460 expecting: false,2461 running: false,2462 session: false,2463 up: true2464 },2465 "w2" ->2466 {2467 attached: Set("c2"),2468 built: false,2469 expecting: true,2470 running: true,2471 session: true,2472 up: true2473 }2474 )2475}24762477[violation] Found an issue (449ms at 40269 traces/second).2478Use --verbosity=3 to show executions.2479Use --seed=0x4263b7f0d6587108 --backend=rust to reproduce.2480error: Invariant violated2481An example execution:24822483[State 0]2484{2485 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2486 schedNoReport::scheduler::crashes: 0,2487 schedNoReport::scheduler::entry: [],2488 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2489 schedNoReport::scheduler::mAssigned: Set(),2490 schedNoReport::scheduler::mBuild: Set(),2491 schedNoReport::scheduler::mDone: Set(),2492 schedNoReport::scheduler::mExpect: Set(),2493 schedNoReport::scheduler::mResult: Set(),2494 schedNoReport::scheduler::mRetry: Set(),2495 schedNoReport::scheduler::mRevoke: Set(),2496 schedNoReport::scheduler::mSchedule: Set(),2497 schedNoReport::scheduler::published: 0,2498 schedNoReport::scheduler::publishedBy: Set(),2499 schedNoReport::scheduler::ws:2500 Map(2501 "w1" ->2502 {2503 attached: Set(),2504 built: false,2505 expecting: false,2506 running: false,2507 session: true,2508 up: true2509 },2510 "w2" ->2511 {2512 attached: Set(),2513 built: false,2514 expecting: false,2515 running: false,2516 session: true,2517 up: true2518 }2519 )2520}25212522[State 1]2523{2524 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2525 schedNoReport::scheduler::crashes: 0,2526 schedNoReport::scheduler::entry: [],2527 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2528 schedNoReport::scheduler::mAssigned: Set(),2529 schedNoReport::scheduler::mBuild: Set(),2530 schedNoReport::scheduler::mDone: Set(),2531 schedNoReport::scheduler::mExpect: Set(),2532 schedNoReport::scheduler::mResult: Set(),2533 schedNoReport::scheduler::mRetry: Set(),2534 schedNoReport::scheduler::mRevoke: Set(),2535 schedNoReport::scheduler::mSchedule: Set("c2"),2536 schedNoReport::scheduler::published: 0,2537 schedNoReport::scheduler::publishedBy: Set(),2538 schedNoReport::scheduler::ws:2539 Map(2540 "w1" ->2541 {2542 attached: Set(),2543 built: false,2544 expecting: false,2545 running: false,2546 session: true,2547 up: true2548 },2549 "w2" ->2550 {2551 attached: Set(),2552 built: false,2553 expecting: false,2554 running: false,2555 session: true,2556 up: true2557 }2558 )2559}25602561[State 2]2562{2563 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2564 schedNoReport::scheduler::crashes: 0,2565 schedNoReport::scheduler::entry:2566 [{ followers: Set("c2"), leased: true, worker: "w2" }],2567 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2568 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2569 schedNoReport::scheduler::mBuild: Set(),2570 schedNoReport::scheduler::mDone: Set(),2571 schedNoReport::scheduler::mExpect: Set("w2"),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: true,2596 up: true2597 }2598 )2599}26002601[State 3]2602{2603 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2604 schedNoReport::scheduler::crashes: 0,2605 schedNoReport::scheduler::entry:2606 [{ followers: Set("c2"), leased: true, worker: "w2" }],2607 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2608 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2609 schedNoReport::scheduler::mBuild: Set(),2610 schedNoReport::scheduler::mDone: Set(),2611 schedNoReport::scheduler::mExpect: Set(),2612 schedNoReport::scheduler::mResult: Set(),2613 schedNoReport::scheduler::mRetry: Set(),2614 schedNoReport::scheduler::mRevoke: Set(),2615 schedNoReport::scheduler::mSchedule: Set(),2616 schedNoReport::scheduler::published: 0,2617 schedNoReport::scheduler::publishedBy: Set(),2618 schedNoReport::scheduler::ws:2619 Map(2620 "w1" ->2621 {2622 attached: Set(),2623 built: false,2624 expecting: false,2625 running: false,2626 session: true,2627 up: true2628 },2629 "w2" ->2630 {2631 attached: Set(),2632 built: false,2633 expecting: true,2634 running: true,2635 session: true,2636 up: true2637 }2638 )2639}26402641[State 4]2642{2643 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2644 schedNoReport::scheduler::crashes: 1,2645 schedNoReport::scheduler::entry:2646 [{ followers: Set("c2"), leased: true, worker: "w2" }],2647 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2648 schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),2649 schedNoReport::scheduler::mBuild: Set(),2650 schedNoReport::scheduler::mDone: Set(),2651 schedNoReport::scheduler::mExpect: Set(),2652 schedNoReport::scheduler::mResult: Set(),2653 schedNoReport::scheduler::mRetry: Set(),2654 schedNoReport::scheduler::mRevoke: Set(),2655 schedNoReport::scheduler::mSchedule: Set(),2656 schedNoReport::scheduler::published: 0,2657 schedNoReport::scheduler::publishedBy: Set(),2658 schedNoReport::scheduler::ws:2659 Map(2660 "w1" ->2661 {2662 attached: Set(),2663 built: false,2664 expecting: false,2665 running: false,2666 session: false,2667 up: false2668 },2669 "w2" ->2670 {2671 attached: Set(),2672 built: false,2673 expecting: true,2674 running: true,2675 session: true,2676 up: true2677 }2678 )2679}26802681[State 5]2682{2683 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2684 schedNoReport::scheduler::crashes: 2,2685 schedNoReport::scheduler::entry: [],2686 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2687 schedNoReport::scheduler::mAssigned: Set(),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("c2"),2693 schedNoReport::scheduler::mRevoke: Set(),2694 schedNoReport::scheduler::mSchedule: Set(),2695 schedNoReport::scheduler::published: 0,2696 schedNoReport::scheduler::publishedBy: Set(),2697 schedNoReport::scheduler::ws:2698 Map(2699 "w1" ->2700 {2701 attached: Set(),2702 built: false,2703 expecting: false,2704 running: false,2705 session: false,2706 up: false2707 },2708 "w2" ->2709 {2710 attached: Set(),2711 built: false,2712 expecting: true,2713 running: true,2714 session: false,2715 up: true2716 }2717 )2718}27192720[State 6]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(),2732 schedNoReport::scheduler::mRevoke: Set(),2733 schedNoReport::scheduler::mSchedule: Set("c2"),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: false,2743 running: false,2744 session: false,2745 up: false2746 },2747 "w2" ->2748 {2749 attached: Set(),2750 built: false,2751 expecting: true,2752 running: true,2753 session: false,2754 up: true2755 }2756 )2757}27582759[State 7]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(),2771 schedNoReport::scheduler::mRevoke: Set(),2772 schedNoReport::scheduler::mSchedule: Set("c2"),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: false,2782 running: false,2783 session: true,2784 up: true2785 },2786 "w2" ->2787 {2788 attached: Set(),2789 built: false,2790 expecting: true,2791 running: true,2792 session: false,2793 up: true2794 }2795 )2796}27972798[State 8]2799{2800 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2801 schedNoReport::scheduler::crashes: 2,2802 schedNoReport::scheduler::entry:2803 [{ followers: Set("c2"), leased: true, worker: "w1" }],2804 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2805 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2806 schedNoReport::scheduler::mBuild: Set(),2807 schedNoReport::scheduler::mDone: Set(),2808 schedNoReport::scheduler::mExpect: Set("w1"),2809 schedNoReport::scheduler::mResult: Set(),2810 schedNoReport::scheduler::mRetry: Set(),2811 schedNoReport::scheduler::mRevoke: Set(),2812 schedNoReport::scheduler::mSchedule: Set(),2813 schedNoReport::scheduler::published: 0,2814 schedNoReport::scheduler::publishedBy: Set(),2815 schedNoReport::scheduler::ws:2816 Map(2817 "w1" ->2818 {2819 attached: Set(),2820 built: false,2821 expecting: false,2822 running: false,2823 session: true,2824 up: true2825 },2826 "w2" ->2827 {2828 attached: Set(),2829 built: false,2830 expecting: true,2831 running: true,2832 session: false,2833 up: true2834 }2835 )2836}28372838[State 9]2839{2840 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2841 schedNoReport::scheduler::crashes: 2,2842 schedNoReport::scheduler::entry:2843 [{ followers: Set("c2"), leased: true, worker: "w1" }],2844 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2845 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2846 schedNoReport::scheduler::mBuild: Set(),2847 schedNoReport::scheduler::mDone: Set(),2848 schedNoReport::scheduler::mExpect: Set(),2849 schedNoReport::scheduler::mResult: Set(),2850 schedNoReport::scheduler::mRetry: Set(),2851 schedNoReport::scheduler::mRevoke: Set(),2852 schedNoReport::scheduler::mSchedule: Set(),2853 schedNoReport::scheduler::published: 0,2854 schedNoReport::scheduler::publishedBy: Set(),2855 schedNoReport::scheduler::ws:2856 Map(2857 "w1" ->2858 {2859 attached: Set(),2860 built: false,2861 expecting: true,2862 running: true,2863 session: true,2864 up: true2865 },2866 "w2" ->2867 {2868 attached: Set(),2869 built: false,2870 expecting: true,2871 running: true,2872 session: false,2873 up: true2874 }2875 )2876}28772878[State 10]2879{2880 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2881 schedNoReport::scheduler::crashes: 2,2882 schedNoReport::scheduler::entry:2883 [{ followers: Set("c2"), leased: true, worker: "w1" }],2884 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2885 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2886 schedNoReport::scheduler::mBuild: Set(),2887 schedNoReport::scheduler::mDone: Set(),2888 schedNoReport::scheduler::mExpect: Set(),2889 schedNoReport::scheduler::mResult: Set(),2890 schedNoReport::scheduler::mRetry: Set(),2891 schedNoReport::scheduler::mRevoke: Set(),2892 schedNoReport::scheduler::mSchedule: Set(),2893 schedNoReport::scheduler::published: 0,2894 schedNoReport::scheduler::publishedBy: Set(),2895 schedNoReport::scheduler::ws:2896 Map(2897 "w1" ->2898 {2899 attached: Set(),2900 built: false,2901 expecting: true,2902 running: true,2903 session: true,2904 up: true2905 },2906 "w2" ->2907 {2908 attached: Set(),2909 built: false,2910 expecting: true,2911 running: true,2912 session: true,2913 up: true2914 }2915 )2916}29172918[violation] Found an issue (446ms at 58814 traces/second).2919Use --verbosity=3 to show executions.2920Use --seed=0x861f01ab3ce3e51 --backend=rust to reproduce.2921error: Invariant violated2922An example execution:29232924[State 0]2925{2926 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2927 schedTerminal::scheduler::crashes: 0,2928 schedTerminal::scheduler::entry: [],2929 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2930 schedTerminal::scheduler::mAssigned: Set(),2931 schedTerminal::scheduler::mBuild: Set(),2932 schedTerminal::scheduler::mDone: Set(),2933 schedTerminal::scheduler::mExpect: Set(),2934 schedTerminal::scheduler::mResult: Set(),2935 schedTerminal::scheduler::mRetry: Set(),2936 schedTerminal::scheduler::mRevoke: Set(),2937 schedTerminal::scheduler::mSchedule: Set(),2938 schedTerminal::scheduler::published: 0,2939 schedTerminal::scheduler::publishedBy: Set(),2940 schedTerminal::scheduler::ws:2941 Map(2942 "w1" ->2943 {2944 attached: Set(),2945 built: false,2946 expecting: false,2947 running: false,2948 session: true,2949 up: true2950 },2951 "w2" ->2952 {2953 attached: Set(),2954 built: false,2955 expecting: false,2956 running: false,2957 session: true,2958 up: true2959 }2960 )2961}29622963[State 1]2964{2965 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2966 schedTerminal::scheduler::crashes: 1,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: false,2988 up: true2989 },2990 "w2" ->2991 {2992 attached: Set(),2993 built: false,2994 expecting: false,2995 running: false,2996 session: false,2997 up: true2998 }2999 )3000}30013002[State 2]3003{3004 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),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("c2"),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 3]3042{3043 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),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(),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[violation] Found an issue (432ms at 4718 traces/second).3081Use --verbosity=3 to show executions.3082Use --seed=0x103ccb80c4535e9c --backend=rust to reproduce.3083error: Invariant violated3084An example execution:30853086[State 0]3087{3088 pushFixed::push::byPath: Map(),3089 pushFixed::push::inflight: Set(),3090 pushFixed::push::left: Map(),3091 pushFixed::push::sent: Map()3092}30933094[State 1]3095{3096 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3097 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3098 pushFixed::push::left: Map(3 -> 2),3099 pushFixed::push::sent: Map(3 -> Set("a", "b"))3100}31013102[State 2]3103{3104 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3105 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (3, "a"), (3, "b")),3106 pushFixed::push::left: Map(1 -> 2, 3 -> 2),3107 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3108}31093110[State 3]3111{3112 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3113 pushFixed::push::inflight:3114 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),3115 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 2),3116 pushFixed::push::sent:3117 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3118}31193120[State 4]3121{3122 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3123 pushFixed::push::inflight:3124 Set((1, "a"), (1, "b"), (2, "a"), (3, "a"), (3, "b")),3125 pushFixed::push::left: Map(1 -> 2, 2 -> 1, 3 -> 2),3126 pushFixed::push::sent:3127 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3128}31293130[State 5]3131{3132 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3133 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (3, "a")),3134 pushFixed::push::left: Map(1 -> 2, 2 -> 1, 3 -> 1),3135 pushFixed::push::sent:3136 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3137}31383139[State 6]3140{3141 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3142 pushFixed::push::inflight: Set((1, "b"), (2, "a"), (3, "a")),3143 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 1),3144 pushFixed::push::sent:3145 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3146}31473148[State 7]3149{3150 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3151 pushFixed::push::inflight: Set((2, "a"), (3, "a")),3152 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1),3153 pushFixed::push::sent:3154 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3155}31563157[State 8]3158{3159 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3160 pushFixed::push::inflight: Set((3, "a")),3161 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1),3162 pushFixed::push::sent:3163 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3164}31653166[State 9]3167{3168 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3169 pushFixed::push::inflight: Set(),3170 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3171 pushFixed::push::sent:3172 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3173}31743175[ok] No violation found (101ms at 198020 traces/second).3176Trace length statistics: max=10, min=7, average=8.123177You may increase --max-samples and --max-steps.3178Use --verbosity to produce more (or less) output.3179Use --seed=0xa0926515648cf79b --backend=rust to reproduce.