nix-grpc-store-spec
checks.x86_64-linux.spec
· build #468
· 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" -> CIdle),46 schedFixed::scheduler::crashes: 1,47 schedFixed::scheduler::entry: [],48 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),49 schedFixed::scheduler::mAssigned: Set(),50 schedFixed::scheduler::mBuild: Set(),51 schedFixed::scheduler::mDone: Set(),52 schedFixed::scheduler::mExpect: Set(),53 schedFixed::scheduler::mResult: Set(),54 schedFixed::scheduler::mRetry: Set(),55 schedFixed::scheduler::mRevoke: Set(),56 schedFixed::scheduler::mSchedule: Set(),57 schedFixed::scheduler::published: 0,58 schedFixed::scheduler::publishedBy: Set(),59 schedFixed::scheduler::ws:60 Map(61 "w1" ->62 {63 attached: Set(),64 built: false,65 expecting: false,66 running: false,67 session: false,68 up: true69 },70 "w2" ->71 {72 attached: Set(),73 built: false,74 expecting: false,75 running: false,76 session: false,77 up: true78 }79 )80}8182[State 2]83{84 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),85 schedFixed::scheduler::crashes: 1,86 schedFixed::scheduler::entry: [],87 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),88 schedFixed::scheduler::mAssigned: Set(),89 schedFixed::scheduler::mBuild: Set(),90 schedFixed::scheduler::mDone: Set(),91 schedFixed::scheduler::mExpect: Set(),92 schedFixed::scheduler::mResult: Set(),93 schedFixed::scheduler::mRetry: Set(),94 schedFixed::scheduler::mRevoke: Set(),95 schedFixed::scheduler::mSchedule: Set(),96 schedFixed::scheduler::published: 0,97 schedFixed::scheduler::publishedBy: Set(),98 schedFixed::scheduler::ws:99 Map(100 "w1" ->101 {102 attached: Set(),103 built: false,104 expecting: false,105 running: false,106 session: true,107 up: true108 },109 "w2" ->110 {111 attached: Set(),112 built: false,113 expecting: false,114 running: false,115 session: false,116 up: true117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),124 schedFixed::scheduler::crashes: 1,125 schedFixed::scheduler::entry: [],126 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),127 schedFixed::scheduler::mAssigned: Set(),128 schedFixed::scheduler::mBuild: Set(),129 schedFixed::scheduler::mDone: Set(),130 schedFixed::scheduler::mExpect: Set(),131 schedFixed::scheduler::mResult: Set(),132 schedFixed::scheduler::mRetry: Set(),133 schedFixed::scheduler::mRevoke: Set(),134 schedFixed::scheduler::mSchedule: Set("c1"),135 schedFixed::scheduler::published: 0,136 schedFixed::scheduler::publishedBy: Set(),137 schedFixed::scheduler::ws:138 Map(139 "w1" ->140 {141 attached: Set(),142 built: false,143 expecting: false,144 running: false,145 session: true,146 up: true147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: true156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),163 schedFixed::scheduler::crashes: 2,164 schedFixed::scheduler::entry: [],165 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),166 schedFixed::scheduler::mAssigned: Set(),167 schedFixed::scheduler::mBuild: Set(),168 schedFixed::scheduler::mDone: Set(),169 schedFixed::scheduler::mExpect: Set(),170 schedFixed::scheduler::mResult: Set(),171 schedFixed::scheduler::mRetry: Set("c1"),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set(),174 schedFixed::scheduler::published: 0,175 schedFixed::scheduler::publishedBy: Set(),176 schedFixed::scheduler::ws:177 Map(178 "w1" ->179 {180 attached: Set(),181 built: false,182 expecting: false,183 running: false,184 session: false,185 up: true186 },187 "w2" ->188 {189 attached: Set(),190 built: false,191 expecting: false,192 running: false,193 session: false,194 up: true195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),202 schedFixed::scheduler::crashes: 2,203 schedFixed::scheduler::entry: [],204 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),205 schedFixed::scheduler::mAssigned: Set(),206 schedFixed::scheduler::mBuild: Set(),207 schedFixed::scheduler::mDone: Set(),208 schedFixed::scheduler::mExpect: Set(),209 schedFixed::scheduler::mResult: Set(),210 schedFixed::scheduler::mRetry: Set("c1"),211 schedFixed::scheduler::mRevoke: Set(),212 schedFixed::scheduler::mSchedule: Set("c2"),213 schedFixed::scheduler::published: 0,214 schedFixed::scheduler::publishedBy: Set(),215 schedFixed::scheduler::ws:216 Map(217 "w1" ->218 {219 attached: Set(),220 built: false,221 expecting: false,222 running: false,223 session: false,224 up: true225 },226 "w2" ->227 {228 attached: Set(),229 built: false,230 expecting: false,231 running: false,232 session: false,233 up: true234 }235 )236}237238[State 6]239{240 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),241 schedFixed::scheduler::crashes: 2,242 schedFixed::scheduler::entry: [],243 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),244 schedFixed::scheduler::mAssigned: Set(),245 schedFixed::scheduler::mBuild: Set(),246 schedFixed::scheduler::mDone: Set(),247 schedFixed::scheduler::mExpect: Set(),248 schedFixed::scheduler::mResult: Set(),249 schedFixed::scheduler::mRetry: Set("c1"),250 schedFixed::scheduler::mRevoke: Set(),251 schedFixed::scheduler::mSchedule: Set("c2"),252 schedFixed::scheduler::published: 0,253 schedFixed::scheduler::publishedBy: Set(),254 schedFixed::scheduler::ws:255 Map(256 "w1" ->257 {258 attached: Set(),259 built: false,260 expecting: false,261 running: false,262 session: true,263 up: true264 },265 "w2" ->266 {267 attached: Set(),268 built: false,269 expecting: false,270 running: false,271 session: false,272 up: true273 }274 )275}276277[State 7]278{279 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),280 schedFixed::scheduler::crashes: 2,281 schedFixed::scheduler::entry: [],282 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),283 schedFixed::scheduler::mAssigned: Set(),284 schedFixed::scheduler::mBuild: Set(),285 schedFixed::scheduler::mDone: Set(),286 schedFixed::scheduler::mExpect: Set(),287 schedFixed::scheduler::mResult: Set(),288 schedFixed::scheduler::mRetry: Set(),289 schedFixed::scheduler::mRevoke: Set(),290 schedFixed::scheduler::mSchedule: Set("c1", "c2"),291 schedFixed::scheduler::published: 0,292 schedFixed::scheduler::publishedBy: Set(),293 schedFixed::scheduler::ws:294 Map(295 "w1" ->296 {297 attached: Set(),298 built: false,299 expecting: false,300 running: false,301 session: true,302 up: true303 },304 "w2" ->305 {306 attached: Set(),307 built: false,308 expecting: false,309 running: false,310 session: false,311 up: true312 }313 )314}315316[State 8]317{318 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),319 schedFixed::scheduler::crashes: 2,320 schedFixed::scheduler::entry:321 [{ followers: Set("c1"), leased: true, worker: "w1" }],322 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),323 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),324 schedFixed::scheduler::mBuild: Set(),325 schedFixed::scheduler::mDone: Set(),326 schedFixed::scheduler::mExpect: Set("w1"),327 schedFixed::scheduler::mResult: Set(),328 schedFixed::scheduler::mRetry: Set(),329 schedFixed::scheduler::mRevoke: Set(),330 schedFixed::scheduler::mSchedule: Set("c2"),331 schedFixed::scheduler::published: 0,332 schedFixed::scheduler::publishedBy: Set(),333 schedFixed::scheduler::ws:334 Map(335 "w1" ->336 {337 attached: Set(),338 built: false,339 expecting: false,340 running: false,341 session: true,342 up: true343 },344 "w2" ->345 {346 attached: Set(),347 built: false,348 expecting: false,349 running: false,350 session: false,351 up: true352 }353 )354}355356[State 9]357{358 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),359 schedFixed::scheduler::crashes: 2,360 schedFixed::scheduler::entry:361 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],362 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),363 schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")),364 schedFixed::scheduler::mBuild: Set(),365 schedFixed::scheduler::mDone: Set(),366 schedFixed::scheduler::mExpect: Set("w1"),367 schedFixed::scheduler::mResult: Set(),368 schedFixed::scheduler::mRetry: Set(),369 schedFixed::scheduler::mRevoke: Set(),370 schedFixed::scheduler::mSchedule: Set(),371 schedFixed::scheduler::published: 0,372 schedFixed::scheduler::publishedBy: Set(),373 schedFixed::scheduler::ws:374 Map(375 "w1" ->376 {377 attached: Set(),378 built: false,379 expecting: false,380 running: false,381 session: true,382 up: true383 },384 "w2" ->385 {386 attached: Set(),387 built: false,388 expecting: false,389 running: false,390 session: false,391 up: true392 }393 )394}395396[State 10]397{398 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),399 schedFixed::scheduler::crashes: 2,400 schedFixed::scheduler::entry:401 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],402 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),403 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),404 schedFixed::scheduler::mBuild: Set(("c1", "w1")),405 schedFixed::scheduler::mDone: Set(),406 schedFixed::scheduler::mExpect: Set("w1"),407 schedFixed::scheduler::mResult: Set(),408 schedFixed::scheduler::mRetry: Set(),409 schedFixed::scheduler::mRevoke: Set(),410 schedFixed::scheduler::mSchedule: Set(),411 schedFixed::scheduler::published: 0,412 schedFixed::scheduler::publishedBy: Set(),413 schedFixed::scheduler::ws:414 Map(415 "w1" ->416 {417 attached: Set(),418 built: false,419 expecting: false,420 running: false,421 session: true,422 up: true423 },424 "w2" ->425 {426 attached: Set(),427 built: false,428 expecting: false,429 running: false,430 session: false,431 up: true432 }433 )434}435436[State 11]437{438 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),439 schedFixed::scheduler::crashes: 2,440 schedFixed::scheduler::entry:441 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],442 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),443 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),444 schedFixed::scheduler::mBuild: Set(("c1", "w1")),445 schedFixed::scheduler::mDone: Set(),446 schedFixed::scheduler::mExpect: Set("w1"),447 schedFixed::scheduler::mResult: Set(),448 schedFixed::scheduler::mRetry: Set(),449 schedFixed::scheduler::mRevoke: Set(),450 schedFixed::scheduler::mSchedule: Set(),451 schedFixed::scheduler::published: 0,452 schedFixed::scheduler::publishedBy: Set(),453 schedFixed::scheduler::ws:454 Map(455 "w1" ->456 {457 attached: Set(),458 built: false,459 expecting: false,460 running: false,461 session: true,462 up: true463 },464 "w2" ->465 {466 attached: Set(),467 built: false,468 expecting: false,469 running: false,470 session: true,471 up: true472 }473 )474}475476[State 12]477{478 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),479 schedFixed::scheduler::crashes: 2,480 schedFixed::scheduler::entry:481 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],482 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),483 schedFixed::scheduler::mAssigned: Set(),484 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),485 schedFixed::scheduler::mDone: Set(),486 schedFixed::scheduler::mExpect: Set("w1"),487 schedFixed::scheduler::mResult: Set(),488 schedFixed::scheduler::mRetry: Set(),489 schedFixed::scheduler::mRevoke: Set(),490 schedFixed::scheduler::mSchedule: Set(),491 schedFixed::scheduler::published: 0,492 schedFixed::scheduler::publishedBy: Set(),493 schedFixed::scheduler::ws:494 Map(495 "w1" ->496 {497 attached: Set(),498 built: false,499 expecting: false,500 running: false,501 session: true,502 up: true503 },504 "w2" ->505 {506 attached: Set(),507 built: false,508 expecting: false,509 running: false,510 session: true,511 up: true512 }513 )514}515516[State 13]517{518 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),519 schedFixed::scheduler::crashes: 2,520 schedFixed::scheduler::entry:521 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],522 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),523 schedFixed::scheduler::mAssigned: Set(),524 schedFixed::scheduler::mBuild: Set(("c2", "w1")),525 schedFixed::scheduler::mDone: Set(),526 schedFixed::scheduler::mExpect: Set("w1"),527 schedFixed::scheduler::mResult: Set(),528 schedFixed::scheduler::mRetry: Set("c1"),529 schedFixed::scheduler::mRevoke: Set(),530 schedFixed::scheduler::mSchedule: Set(),531 schedFixed::scheduler::published: 0,532 schedFixed::scheduler::publishedBy: Set(),533 schedFixed::scheduler::ws:534 Map(535 "w1" ->536 {537 attached: Set(),538 built: false,539 expecting: false,540 running: false,541 session: true,542 up: true543 },544 "w2" ->545 {546 attached: Set(),547 built: false,548 expecting: false,549 running: false,550 session: true,551 up: true552 }553 )554}555556[State 14]557{558 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),559 schedFixed::scheduler::crashes: 2,560 schedFixed::scheduler::entry:561 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],562 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),563 schedFixed::scheduler::mAssigned: Set(),564 schedFixed::scheduler::mBuild: Set(),565 schedFixed::scheduler::mDone: Set(),566 schedFixed::scheduler::mExpect: Set("w1"),567 schedFixed::scheduler::mResult: Set(),568 schedFixed::scheduler::mRetry: Set("c1", "c2"),569 schedFixed::scheduler::mRevoke: Set(),570 schedFixed::scheduler::mSchedule: Set(),571 schedFixed::scheduler::published: 0,572 schedFixed::scheduler::publishedBy: Set(),573 schedFixed::scheduler::ws:574 Map(575 "w1" ->576 {577 attached: Set(),578 built: false,579 expecting: false,580 running: false,581 session: true,582 up: true583 },584 "w2" ->585 {586 attached: Set(),587 built: false,588 expecting: false,589 running: false,590 session: true,591 up: true592 }593 )594}595596[State 15]597{598 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),599 schedFixed::scheduler::crashes: 2,600 schedFixed::scheduler::entry:601 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],602 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),603 schedFixed::scheduler::mAssigned: Set(),604 schedFixed::scheduler::mBuild: Set(),605 schedFixed::scheduler::mDone: Set(),606 schedFixed::scheduler::mExpect: Set("w1"),607 schedFixed::scheduler::mResult: Set(),608 schedFixed::scheduler::mRetry: Set("c2"),609 schedFixed::scheduler::mRevoke: Set(),610 schedFixed::scheduler::mSchedule: Set("c1"),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" -> CSent("w1")),639 schedFixed::scheduler::crashes: 2,640 schedFixed::scheduler::entry:641 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],642 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),643 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),644 schedFixed::scheduler::mBuild: Set(),645 schedFixed::scheduler::mDone: Set(),646 schedFixed::scheduler::mExpect: Set("w1"),647 schedFixed::scheduler::mResult: Set(),648 schedFixed::scheduler::mRetry: Set("c2"),649 schedFixed::scheduler::mRevoke: Set(),650 schedFixed::scheduler::mSchedule: Set(),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" -> CSent("w1"), "c2" -> CSent("w1")),679 schedFixed::scheduler::crashes: 2,680 schedFixed::scheduler::entry:681 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],682 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),683 schedFixed::scheduler::mAssigned: Set(),684 schedFixed::scheduler::mBuild: Set(("c1", "w1")),685 schedFixed::scheduler::mDone: Set(),686 schedFixed::scheduler::mExpect: Set("w1"),687 schedFixed::scheduler::mResult: Set(),688 schedFixed::scheduler::mRetry: Set("c2"),689 schedFixed::scheduler::mRevoke: Set(),690 schedFixed::scheduler::mSchedule: Set(),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" -> CSent("w1"), "c2" -> CQueued),719 schedFixed::scheduler::crashes: 2,720 schedFixed::scheduler::entry:721 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],722 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),723 schedFixed::scheduler::mAssigned: Set(),724 schedFixed::scheduler::mBuild: Set(("c1", "w1")),725 schedFixed::scheduler::mDone: Set(),726 schedFixed::scheduler::mExpect: Set("w1"),727 schedFixed::scheduler::mResult: Set(),728 schedFixed::scheduler::mRetry: Set(),729 schedFixed::scheduler::mRevoke: Set(),730 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CSent("w1"), "c2" -> CQueued),759 schedFixed::scheduler::crashes: 2,760 schedFixed::scheduler::entry:761 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],762 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),763 schedFixed::scheduler::mAssigned: Set(),764 schedFixed::scheduler::mBuild: Set(),765 schedFixed::scheduler::mDone: Set(),766 schedFixed::scheduler::mExpect: Set("w1"),767 schedFixed::scheduler::mResult: Set(),768 schedFixed::scheduler::mRetry: Set("c1"),769 schedFixed::scheduler::mRevoke: Set(),770 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CQueued),799 schedFixed::scheduler::crashes: 2,800 schedFixed::scheduler::entry:801 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],802 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),803 schedFixed::scheduler::mAssigned: Set(),804 schedFixed::scheduler::mBuild: Set(),805 schedFixed::scheduler::mDone: Set(),806 schedFixed::scheduler::mExpect: Set("w1"),807 schedFixed::scheduler::mResult: Set(),808 schedFixed::scheduler::mRetry: Set(),809 schedFixed::scheduler::mRevoke: Set(),810 schedFixed::scheduler::mSchedule: Set("c1", "c2"),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" -> CQueued),839 schedFixed::scheduler::crashes: 2,840 schedFixed::scheduler::entry:841 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],842 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),843 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),844 schedFixed::scheduler::mBuild: Set(),845 schedFixed::scheduler::mDone: Set(),846 schedFixed::scheduler::mExpect: Set("w1"),847 schedFixed::scheduler::mResult: Set(),848 schedFixed::scheduler::mRetry: Set(),849 schedFixed::scheduler::mRevoke: Set(),850 schedFixed::scheduler::mSchedule: Set("c2"),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" -> CSent("w1"), "c2" -> CQueued),879 schedFixed::scheduler::crashes: 2,880 schedFixed::scheduler::entry:881 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],882 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),883 schedFixed::scheduler::mAssigned: Set(),884 schedFixed::scheduler::mBuild: Set(("c1", "w1")),885 schedFixed::scheduler::mDone: Set(),886 schedFixed::scheduler::mExpect: Set("w1"),887 schedFixed::scheduler::mResult: Set(),888 schedFixed::scheduler::mRetry: Set(),889 schedFixed::scheduler::mRevoke: Set(),890 schedFixed::scheduler::mSchedule: Set("c2"),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: false,909 running: false,910 session: true,911 up: true912 }913 )914}915916[State 23]917{918 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),919 schedFixed::scheduler::crashes: 2,920 schedFixed::scheduler::entry:921 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],922 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),923 schedFixed::scheduler::mAssigned: Set(("c2", "w1")),924 schedFixed::scheduler::mBuild: Set(("c1", "w1")),925 schedFixed::scheduler::mDone: Set(),926 schedFixed::scheduler::mExpect: Set("w1"),927 schedFixed::scheduler::mResult: Set(),928 schedFixed::scheduler::mRetry: Set(),929 schedFixed::scheduler::mRevoke: Set(),930 schedFixed::scheduler::mSchedule: Set(),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: false,949 running: false,950 session: true,951 up: true952 }953 )954}955956[State 24]957{958 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),959 schedFixed::scheduler::crashes: 2,960 schedFixed::scheduler::entry:961 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],962 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),963 schedFixed::scheduler::mAssigned: Set(),964 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),965 schedFixed::scheduler::mDone: Set(),966 schedFixed::scheduler::mExpect: Set("w1"),967 schedFixed::scheduler::mResult: Set(),968 schedFixed::scheduler::mRetry: Set(),969 schedFixed::scheduler::mRevoke: Set(),970 schedFixed::scheduler::mSchedule: Set(),971 schedFixed::scheduler::published: 0,972 schedFixed::scheduler::publishedBy: Set(),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: false,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("w1"), "c2" -> CSent("w1")),999 schedFixed::scheduler::crashes: 2,1000 schedFixed::scheduler::entry:1001 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1002 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1003 schedFixed::scheduler::mAssigned: Set(),1004 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1005 schedFixed::scheduler::mDone: Set(),1006 schedFixed::scheduler::mExpect: Set("w1"),1007 schedFixed::scheduler::mResult: Set(),1008 schedFixed::scheduler::mRetry: Set("c1"),1009 schedFixed::scheduler::mRevoke: Set(),1010 schedFixed::scheduler::mSchedule: Set(),1011 schedFixed::scheduler::published: 0,1012 schedFixed::scheduler::publishedBy: Set(),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: false,1028 expecting: false,1029 running: false,1030 session: true,1031 up: true1032 }1033 )1034}10351036[State 26]1037{1038 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),1039 schedFixed::scheduler::crashes: 2,1040 schedFixed::scheduler::entry:1041 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1042 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1043 schedFixed::scheduler::mAssigned: Set(),1044 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1045 schedFixed::scheduler::mDone: Set(),1046 schedFixed::scheduler::mExpect: Set("w1"),1047 schedFixed::scheduler::mResult: Set(),1048 schedFixed::scheduler::mRetry: Set(),1049 schedFixed::scheduler::mRevoke: Set(),1050 schedFixed::scheduler::mSchedule: Set("c1"),1051 schedFixed::scheduler::published: 0,1052 schedFixed::scheduler::publishedBy: Set(),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: false,1068 expecting: false,1069 running: false,1070 session: true,1071 up: true1072 }1073 )1074}10751076[State 27]1077{1078 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),1079 schedFixed::scheduler::crashes: 2,1080 schedFixed::scheduler::entry:1081 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1082 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1083 schedFixed::scheduler::mAssigned: Set(),1084 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1085 schedFixed::scheduler::mDone: Set(),1086 schedFixed::scheduler::mExpect: Set(),1087 schedFixed::scheduler::mResult: Set(),1088 schedFixed::scheduler::mRetry: Set(),1089 schedFixed::scheduler::mRevoke: Set(),1090 schedFixed::scheduler::mSchedule: Set("c1"),1091 schedFixed::scheduler::published: 0,1092 schedFixed::scheduler::publishedBy: Set(),1093 schedFixed::scheduler::ws:1094 Map(1095 "w1" ->1096 {1097 attached: Set(),1098 built: false,1099 expecting: true,1100 running: true,1101 session: true,1102 up: true1103 },1104 "w2" ->1105 {1106 attached: Set(),1107 built: false,1108 expecting: false,1109 running: false,1110 session: true,1111 up: true1112 }1113 )1114}11151116[State 28]1117{1118 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),1119 schedFixed::scheduler::crashes: 2,1120 schedFixed::scheduler::entry:1121 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1122 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1123 schedFixed::scheduler::mAssigned: Set(("c1", "w1")),1124 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1125 schedFixed::scheduler::mDone: Set(),1126 schedFixed::scheduler::mExpect: Set(),1127 schedFixed::scheduler::mResult: Set(),1128 schedFixed::scheduler::mRetry: Set(),1129 schedFixed::scheduler::mRevoke: Set(),1130 schedFixed::scheduler::mSchedule: Set(),1131 schedFixed::scheduler::published: 0,1132 schedFixed::scheduler::publishedBy: Set(),1133 schedFixed::scheduler::ws:1134 Map(1135 "w1" ->1136 {1137 attached: Set(),1138 built: false,1139 expecting: true,1140 running: true,1141 session: true,1142 up: true1143 },1144 "w2" ->1145 {1146 attached: Set(),1147 built: false,1148 expecting: false,1149 running: false,1150 session: true,1151 up: true1152 }1153 )1154}11551156[State 29]1157{1158 schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),1159 schedFixed::scheduler::crashes: 2,1160 schedFixed::scheduler::entry:1161 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1162 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1163 schedFixed::scheduler::mAssigned: Set(),1164 schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")),1165 schedFixed::scheduler::mDone: Set(),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: 0,1172 schedFixed::scheduler::publishedBy: Set(),1173 schedFixed::scheduler::ws:1174 Map(1175 "w1" ->1176 {1177 attached: Set(),1178 built: false,1179 expecting: true,1180 running: true,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" -> CSent("w1"), "c2" -> CSent("w1")),1199 schedFixed::scheduler::crashes: 2,1200 schedFixed::scheduler::entry:1201 [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],1202 schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),1203 schedFixed::scheduler::mAssigned: Set(),1204 schedFixed::scheduler::mBuild: Set(("c1", "w1")),1205 schedFixed::scheduler::mDone: Set(),1206 schedFixed::scheduler::mExpect: Set(),1207 schedFixed::scheduler::mResult: Set(),1208 schedFixed::scheduler::mRetry: Set(),1209 schedFixed::scheduler::mRevoke: Set(),1210 schedFixed::scheduler::mSchedule: Set(),1211 schedFixed::scheduler::published: 0,1212 schedFixed::scheduler::publishedBy: Set(),1213 schedFixed::scheduler::ws:1214 Map(1215 "w1" ->1216 {1217 attached: Set("c2"),1218 built: false,1219 expecting: true,1220 running: true,1221 session: true,1222 up: true1223 },1224 "w2" ->1225 {1226 attached: Set(),1227 built: false,1228 expecting: false,1229 running: false,1230 session: true,1231 up: true1232 }1233 )1234}12351236[ok] No violation found (472ms at 63559 traces/second).1237Trace length statistics: max=26, min=16, average=18.761238You may increase --max-samples and --max-steps.1239Use --verbosity to produce more (or less) output.1240Use --seed=0x605006d41b91420b --backend=rust to reproduce.1241An example execution:12421243[State 0]1244{1245 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1246 schedNoRevoke::scheduler::crashes: 0,1247 schedNoRevoke::scheduler::entry: [],1248 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1249 schedNoRevoke::scheduler::mAssigned: Set(),1250 schedNoRevoke::scheduler::mBuild: Set(),1251 schedNoRevoke::scheduler::mDone: Set(),1252 schedNoRevoke::scheduler::mExpect: Set(),1253 schedNoRevoke::scheduler::mResult: Set(),1254 schedNoRevoke::scheduler::mRetry: Set(),1255 schedNoRevoke::scheduler::mRevoke: Set(),1256 schedNoRevoke::scheduler::mSchedule: Set(),1257 schedNoRevoke::scheduler::published: 0,1258 schedNoRevoke::scheduler::publishedBy: Set(),1259 schedNoRevoke::scheduler::ws:1260 Map(1261 "w1" ->1262 {1263 attached: Set(),1264 built: false,1265 expecting: false,1266 running: false,1267 session: true,1268 up: true1269 },1270 "w2" ->1271 {1272 attached: Set(),1273 built: false,1274 expecting: false,1275 running: false,1276 session: true,1277 up: true1278 }1279 )1280}12811282[State 1]1283{1284 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1285 schedNoRevoke::scheduler::crashes: 0,1286 schedNoRevoke::scheduler::entry: [],1287 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1288 schedNoRevoke::scheduler::mAssigned: Set(),1289 schedNoRevoke::scheduler::mBuild: Set(),1290 schedNoRevoke::scheduler::mDone: Set(),1291 schedNoRevoke::scheduler::mExpect: Set(),1292 schedNoRevoke::scheduler::mResult: Set(),1293 schedNoRevoke::scheduler::mRetry: Set(),1294 schedNoRevoke::scheduler::mRevoke: Set(),1295 schedNoRevoke::scheduler::mSchedule: Set("c1"),1296 schedNoRevoke::scheduler::published: 0,1297 schedNoRevoke::scheduler::publishedBy: Set(),1298 schedNoRevoke::scheduler::ws:1299 Map(1300 "w1" ->1301 {1302 attached: Set(),1303 built: false,1304 expecting: false,1305 running: false,1306 session: true,1307 up: true1308 },1309 "w2" ->1310 {1311 attached: Set(),1312 built: false,1313 expecting: false,1314 running: false,1315 session: true,1316 up: true1317 }1318 )1319}13201321[State 2]1322{1323 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1324 schedNoRevoke::scheduler::crashes: 0,1325 schedNoRevoke::scheduler::entry:1326 [{ followers: Set("c1"), leased: true, worker: "w1" }],1327 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1328 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1329 schedNoRevoke::scheduler::mBuild: Set(),1330 schedNoRevoke::scheduler::mDone: Set(),1331 schedNoRevoke::scheduler::mExpect: Set("w1"),1332 schedNoRevoke::scheduler::mResult: Set(),1333 schedNoRevoke::scheduler::mRetry: Set(),1334 schedNoRevoke::scheduler::mRevoke: Set(),1335 schedNoRevoke::scheduler::mSchedule: Set(),1336 schedNoRevoke::scheduler::published: 0,1337 schedNoRevoke::scheduler::publishedBy: Set(),1338 schedNoRevoke::scheduler::ws:1339 Map(1340 "w1" ->1341 {1342 attached: Set(),1343 built: false,1344 expecting: false,1345 running: false,1346 session: true,1347 up: true1348 },1349 "w2" ->1350 {1351 attached: Set(),1352 built: false,1353 expecting: false,1354 running: false,1355 session: true,1356 up: true1357 }1358 )1359}13601361[State 3]1362{1363 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1364 schedNoRevoke::scheduler::crashes: 0,1365 schedNoRevoke::scheduler::entry:1366 [{ followers: Set("c1"), leased: true, worker: "w1" }],1367 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1368 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1369 schedNoRevoke::scheduler::mBuild: Set(),1370 schedNoRevoke::scheduler::mDone: Set(),1371 schedNoRevoke::scheduler::mExpect: Set(),1372 schedNoRevoke::scheduler::mResult: Set(),1373 schedNoRevoke::scheduler::mRetry: Set(),1374 schedNoRevoke::scheduler::mRevoke: Set(),1375 schedNoRevoke::scheduler::mSchedule: Set(),1376 schedNoRevoke::scheduler::published: 0,1377 schedNoRevoke::scheduler::publishedBy: Set(),1378 schedNoRevoke::scheduler::ws:1379 Map(1380 "w1" ->1381 {1382 attached: Set(),1383 built: false,1384 expecting: true,1385 running: true,1386 session: true,1387 up: true1388 },1389 "w2" ->1390 {1391 attached: Set(),1392 built: false,1393 expecting: false,1394 running: false,1395 session: true,1396 up: true1397 }1398 )1399}14001401[State 4]1402{1403 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1404 schedNoRevoke::scheduler::crashes: 1,1405 schedNoRevoke::scheduler::entry:1406 [{ followers: Set("c1"), leased: true, worker: "w1" }],1407 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1408 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w1")),1409 schedNoRevoke::scheduler::mBuild: Set(),1410 schedNoRevoke::scheduler::mDone: Set(),1411 schedNoRevoke::scheduler::mExpect: Set(),1412 schedNoRevoke::scheduler::mResult: Set(),1413 schedNoRevoke::scheduler::mRetry: Set(),1414 schedNoRevoke::scheduler::mRevoke: Set(),1415 schedNoRevoke::scheduler::mSchedule: Set(),1416 schedNoRevoke::scheduler::published: 0,1417 schedNoRevoke::scheduler::publishedBy: Set(),1418 schedNoRevoke::scheduler::ws:1419 Map(1420 "w1" ->1421 {1422 attached: Set(),1423 built: false,1424 expecting: true,1425 running: true,1426 session: true,1427 up: true1428 },1429 "w2" ->1430 {1431 attached: Set(),1432 built: false,1433 expecting: false,1434 running: false,1435 session: false,1436 up: false1437 }1438 )1439}14401441[State 5]1442{1443 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1444 schedNoRevoke::scheduler::crashes: 2,1445 schedNoRevoke::scheduler::entry: [],1446 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1447 schedNoRevoke::scheduler::mAssigned: Set(),1448 schedNoRevoke::scheduler::mBuild: Set(),1449 schedNoRevoke::scheduler::mDone: Set(),1450 schedNoRevoke::scheduler::mExpect: Set(),1451 schedNoRevoke::scheduler::mResult: Set(),1452 schedNoRevoke::scheduler::mRetry: Set("c1"),1453 schedNoRevoke::scheduler::mRevoke: Set(),1454 schedNoRevoke::scheduler::mSchedule: Set(),1455 schedNoRevoke::scheduler::published: 0,1456 schedNoRevoke::scheduler::publishedBy: Set(),1457 schedNoRevoke::scheduler::ws:1458 Map(1459 "w1" ->1460 {1461 attached: Set(),1462 built: false,1463 expecting: true,1464 running: true,1465 session: false,1466 up: true1467 },1468 "w2" ->1469 {1470 attached: Set(),1471 built: false,1472 expecting: false,1473 running: false,1474 session: false,1475 up: false1476 }1477 )1478}14791480[State 6]1481{1482 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1483 schedNoRevoke::scheduler::crashes: 2,1484 schedNoRevoke::scheduler::entry: [],1485 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1486 schedNoRevoke::scheduler::mAssigned: Set(),1487 schedNoRevoke::scheduler::mBuild: Set(),1488 schedNoRevoke::scheduler::mDone: Set(),1489 schedNoRevoke::scheduler::mExpect: Set(),1490 schedNoRevoke::scheduler::mResult: Set(),1491 schedNoRevoke::scheduler::mRetry: Set("c1"),1492 schedNoRevoke::scheduler::mRevoke: Set(),1493 schedNoRevoke::scheduler::mSchedule: Set("c2"),1494 schedNoRevoke::scheduler::published: 0,1495 schedNoRevoke::scheduler::publishedBy: Set(),1496 schedNoRevoke::scheduler::ws:1497 Map(1498 "w1" ->1499 {1500 attached: Set(),1501 built: false,1502 expecting: true,1503 running: true,1504 session: false,1505 up: true1506 },1507 "w2" ->1508 {1509 attached: Set(),1510 built: false,1511 expecting: false,1512 running: false,1513 session: false,1514 up: false1515 }1516 )1517}15181519[State 7]1520{1521 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1522 schedNoRevoke::scheduler::crashes: 2,1523 schedNoRevoke::scheduler::entry: [],1524 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1525 schedNoRevoke::scheduler::mAssigned: Set(),1526 schedNoRevoke::scheduler::mBuild: Set(),1527 schedNoRevoke::scheduler::mDone: Set(),1528 schedNoRevoke::scheduler::mExpect: Set(),1529 schedNoRevoke::scheduler::mResult: Set(),1530 schedNoRevoke::scheduler::mRetry: Set("c1"),1531 schedNoRevoke::scheduler::mRevoke: Set(),1532 schedNoRevoke::scheduler::mSchedule: Set("c2"),1533 schedNoRevoke::scheduler::published: 0,1534 schedNoRevoke::scheduler::publishedBy: Set(),1535 schedNoRevoke::scheduler::ws:1536 Map(1537 "w1" ->1538 {1539 attached: Set(),1540 built: false,1541 expecting: true,1542 running: true,1543 session: false,1544 up: true1545 },1546 "w2" ->1547 {1548 attached: Set(),1549 built: false,1550 expecting: false,1551 running: false,1552 session: true,1553 up: true1554 }1555 )1556}15571558[State 8]1559{1560 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1561 schedNoRevoke::scheduler::crashes: 2,1562 schedNoRevoke::scheduler::entry:1563 [{ followers: Set("c2"), leased: true, worker: "w2" }],1564 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1565 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1566 schedNoRevoke::scheduler::mBuild: Set(),1567 schedNoRevoke::scheduler::mDone: Set(),1568 schedNoRevoke::scheduler::mExpect: Set("w2"),1569 schedNoRevoke::scheduler::mResult: Set(),1570 schedNoRevoke::scheduler::mRetry: Set("c1"),1571 schedNoRevoke::scheduler::mRevoke: Set(),1572 schedNoRevoke::scheduler::mSchedule: Set(),1573 schedNoRevoke::scheduler::published: 0,1574 schedNoRevoke::scheduler::publishedBy: Set(),1575 schedNoRevoke::scheduler::ws:1576 Map(1577 "w1" ->1578 {1579 attached: Set(),1580 built: false,1581 expecting: true,1582 running: true,1583 session: false,1584 up: true1585 },1586 "w2" ->1587 {1588 attached: Set(),1589 built: false,1590 expecting: false,1591 running: false,1592 session: true,1593 up: true1594 }1595 )1596}15971598[State 9]1599{1600 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1601 schedNoRevoke::scheduler::crashes: 2,1602 schedNoRevoke::scheduler::entry:1603 [{ followers: Set("c2"), leased: true, worker: "w2" }],1604 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1605 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1606 schedNoRevoke::scheduler::mBuild: Set(),1607 schedNoRevoke::scheduler::mDone: Set(),1608 schedNoRevoke::scheduler::mExpect: Set(),1609 schedNoRevoke::scheduler::mResult: Set(),1610 schedNoRevoke::scheduler::mRetry: Set("c1"),1611 schedNoRevoke::scheduler::mRevoke: Set(),1612 schedNoRevoke::scheduler::mSchedule: Set(),1613 schedNoRevoke::scheduler::published: 0,1614 schedNoRevoke::scheduler::publishedBy: Set(),1615 schedNoRevoke::scheduler::ws:1616 Map(1617 "w1" ->1618 {1619 attached: Set(),1620 built: false,1621 expecting: true,1622 running: true,1623 session: false,1624 up: true1625 },1626 "w2" ->1627 {1628 attached: Set(),1629 built: false,1630 expecting: true,1631 running: true,1632 session: true,1633 up: true1634 }1635 )1636}16371638[State 10]1639{1640 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1641 schedNoRevoke::scheduler::crashes: 2,1642 schedNoRevoke::scheduler::entry:1643 [{ followers: Set("c2"), leased: true, worker: "w2" }],1644 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1645 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w2")),1646 schedNoRevoke::scheduler::mBuild: Set(),1647 schedNoRevoke::scheduler::mDone: Set(),1648 schedNoRevoke::scheduler::mExpect: Set(),1649 schedNoRevoke::scheduler::mResult: Set(),1650 schedNoRevoke::scheduler::mRetry: Set("c1"),1651 schedNoRevoke::scheduler::mRevoke: Set(),1652 schedNoRevoke::scheduler::mSchedule: Set(),1653 schedNoRevoke::scheduler::published: 0,1654 schedNoRevoke::scheduler::publishedBy: Set(),1655 schedNoRevoke::scheduler::ws:1656 Map(1657 "w1" ->1658 {1659 attached: Set(),1660 built: false,1661 expecting: true,1662 running: true,1663 session: true,1664 up: true1665 },1666 "w2" ->1667 {1668 attached: Set(),1669 built: false,1670 expecting: true,1671 running: true,1672 session: true,1673 up: true1674 }1675 )1676}16771678[violation] Found an issue (453ms at 64581 traces/second).1679Use --verbosity=3 to show executions.1680Use --seed=0xf2a1c9cead7bd1f9 --backend=rust to reproduce.1681error: Invariant violated1682An example execution:16831684[State 0]1685{1686 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1687 schedNoFence::scheduler::crashes: 0,1688 schedNoFence::scheduler::entry: [],1689 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1690 schedNoFence::scheduler::mAssigned: Set(),1691 schedNoFence::scheduler::mBuild: Set(),1692 schedNoFence::scheduler::mDone: Set(),1693 schedNoFence::scheduler::mExpect: Set(),1694 schedNoFence::scheduler::mResult: Set(),1695 schedNoFence::scheduler::mRetry: Set(),1696 schedNoFence::scheduler::mRevoke: Set(),1697 schedNoFence::scheduler::mSchedule: Set(),1698 schedNoFence::scheduler::published: 0,1699 schedNoFence::scheduler::publishedBy: Set(),1700 schedNoFence::scheduler::ws:1701 Map(1702 "w1" ->1703 {1704 attached: Set(),1705 built: false,1706 expecting: false,1707 running: false,1708 session: true,1709 up: true1710 },1711 "w2" ->1712 {1713 attached: Set(),1714 built: false,1715 expecting: false,1716 running: false,1717 session: true,1718 up: true1719 }1720 )1721}17221723[State 1]1724{1725 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1726 schedNoFence::scheduler::crashes: 0,1727 schedNoFence::scheduler::entry: [],1728 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1729 schedNoFence::scheduler::mAssigned: Set(),1730 schedNoFence::scheduler::mBuild: Set(),1731 schedNoFence::scheduler::mDone: Set(),1732 schedNoFence::scheduler::mExpect: Set(),1733 schedNoFence::scheduler::mResult: Set(),1734 schedNoFence::scheduler::mRetry: Set(),1735 schedNoFence::scheduler::mRevoke: Set(),1736 schedNoFence::scheduler::mSchedule: Set("c1"),1737 schedNoFence::scheduler::published: 0,1738 schedNoFence::scheduler::publishedBy: Set(),1739 schedNoFence::scheduler::ws:1740 Map(1741 "w1" ->1742 {1743 attached: Set(),1744 built: false,1745 expecting: false,1746 running: false,1747 session: true,1748 up: true1749 },1750 "w2" ->1751 {1752 attached: Set(),1753 built: false,1754 expecting: false,1755 running: false,1756 session: true,1757 up: true1758 }1759 )1760}17611762[State 2]1763{1764 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1765 schedNoFence::scheduler::crashes: 1,1766 schedNoFence::scheduler::entry: [],1767 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1768 schedNoFence::scheduler::mAssigned: Set(),1769 schedNoFence::scheduler::mBuild: Set(),1770 schedNoFence::scheduler::mDone: Set(),1771 schedNoFence::scheduler::mExpect: Set(),1772 schedNoFence::scheduler::mResult: Set(),1773 schedNoFence::scheduler::mRetry: Set(),1774 schedNoFence::scheduler::mRevoke: Set(),1775 schedNoFence::scheduler::mSchedule: Set("c1"),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: false,1796 up: false1797 }1798 )1799}18001801[State 3]1802{1803 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1804 schedNoFence::scheduler::crashes: 1,1805 schedNoFence::scheduler::entry:1806 [{ followers: Set("c1"), leased: true, worker: "w1" }],1807 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1808 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1809 schedNoFence::scheduler::mBuild: Set(),1810 schedNoFence::scheduler::mDone: Set(),1811 schedNoFence::scheduler::mExpect: Set("w1"),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: false,1825 running: false,1826 session: true,1827 up: true1828 },1829 "w2" ->1830 {1831 attached: Set(),1832 built: false,1833 expecting: false,1834 running: false,1835 session: false,1836 up: false1837 }1838 )1839}18401841[State 4]1842{1843 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1844 schedNoFence::scheduler::crashes: 1,1845 schedNoFence::scheduler::entry:1846 [{ followers: Set("c1"), leased: true, worker: "w1" }],1847 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1848 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1849 schedNoFence::scheduler::mBuild: Set(),1850 schedNoFence::scheduler::mDone: Set(),1851 schedNoFence::scheduler::mExpect: Set(),1852 schedNoFence::scheduler::mResult: Set(),1853 schedNoFence::scheduler::mRetry: Set(),1854 schedNoFence::scheduler::mRevoke: Set(),1855 schedNoFence::scheduler::mSchedule: Set(),1856 schedNoFence::scheduler::published: 0,1857 schedNoFence::scheduler::publishedBy: Set(),1858 schedNoFence::scheduler::ws:1859 Map(1860 "w1" ->1861 {1862 attached: Set(),1863 built: false,1864 expecting: true,1865 running: true,1866 session: true,1867 up: true1868 },1869 "w2" ->1870 {1871 attached: Set(),1872 built: false,1873 expecting: false,1874 running: false,1875 session: false,1876 up: false1877 }1878 )1879}18801881[State 5]1882{1883 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1884 schedNoFence::scheduler::crashes: 2,1885 schedNoFence::scheduler::entry: [],1886 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1887 schedNoFence::scheduler::mAssigned: Set(),1888 schedNoFence::scheduler::mBuild: Set(),1889 schedNoFence::scheduler::mDone: Set(),1890 schedNoFence::scheduler::mExpect: Set(),1891 schedNoFence::scheduler::mResult: Set(),1892 schedNoFence::scheduler::mRetry: Set("c1"),1893 schedNoFence::scheduler::mRevoke: Set(),1894 schedNoFence::scheduler::mSchedule: Set(),1895 schedNoFence::scheduler::published: 0,1896 schedNoFence::scheduler::publishedBy: Set(),1897 schedNoFence::scheduler::ws:1898 Map(1899 "w1" ->1900 {1901 attached: Set(),1902 built: false,1903 expecting: true,1904 running: true,1905 session: false,1906 up: true1907 },1908 "w2" ->1909 {1910 attached: Set(),1911 built: false,1912 expecting: false,1913 running: false,1914 session: false,1915 up: false1916 }1917 )1918}19191920[State 6]1921{1922 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1923 schedNoFence::scheduler::crashes: 2,1924 schedNoFence::scheduler::entry: [],1925 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1926 schedNoFence::scheduler::mAssigned: Set(),1927 schedNoFence::scheduler::mBuild: Set(),1928 schedNoFence::scheduler::mDone: Set(),1929 schedNoFence::scheduler::mExpect: Set(),1930 schedNoFence::scheduler::mResult: Set(),1931 schedNoFence::scheduler::mRetry: Set("c1"),1932 schedNoFence::scheduler::mRevoke: Set(),1933 schedNoFence::scheduler::mSchedule: Set(),1934 schedNoFence::scheduler::published: 0,1935 schedNoFence::scheduler::publishedBy: Set(),1936 schedNoFence::scheduler::ws:1937 Map(1938 "w1" ->1939 {1940 attached: Set(),1941 built: false,1942 expecting: true,1943 running: true,1944 session: false,1945 up: true1946 },1947 "w2" ->1948 {1949 attached: Set(),1950 built: false,1951 expecting: false,1952 running: false,1953 session: true,1954 up: true1955 }1956 )1957}19581959[State 7]1960{1961 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1962 schedNoFence::scheduler::crashes: 2,1963 schedNoFence::scheduler::entry: [],1964 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1965 schedNoFence::scheduler::mAssigned: Set(),1966 schedNoFence::scheduler::mBuild: Set(),1967 schedNoFence::scheduler::mDone: Set(),1968 schedNoFence::scheduler::mExpect: Set(),1969 schedNoFence::scheduler::mResult: Set(),1970 schedNoFence::scheduler::mRetry: Set("c1"),1971 schedNoFence::scheduler::mRevoke: Set(),1972 schedNoFence::scheduler::mSchedule: Set("c2"),1973 schedNoFence::scheduler::published: 0,1974 schedNoFence::scheduler::publishedBy: Set(),1975 schedNoFence::scheduler::ws:1976 Map(1977 "w1" ->1978 {1979 attached: Set(),1980 built: false,1981 expecting: true,1982 running: true,1983 session: false,1984 up: true1985 },1986 "w2" ->1987 {1988 attached: Set(),1989 built: false,1990 expecting: false,1991 running: false,1992 session: true,1993 up: true1994 }1995 )1996}19971998[State 8]1999{2000 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2001 schedNoFence::scheduler::crashes: 2,2002 schedNoFence::scheduler::entry:2003 [{ followers: Set("c2"), leased: true, worker: "w2" }],2004 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2005 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2006 schedNoFence::scheduler::mBuild: Set(),2007 schedNoFence::scheduler::mDone: Set(),2008 schedNoFence::scheduler::mExpect: Set("w2"),2009 schedNoFence::scheduler::mResult: Set(),2010 schedNoFence::scheduler::mRetry: Set("c1"),2011 schedNoFence::scheduler::mRevoke: Set(),2012 schedNoFence::scheduler::mSchedule: Set(),2013 schedNoFence::scheduler::published: 0,2014 schedNoFence::scheduler::publishedBy: Set(),2015 schedNoFence::scheduler::ws:2016 Map(2017 "w1" ->2018 {2019 attached: Set(),2020 built: false,2021 expecting: true,2022 running: true,2023 session: false,2024 up: true2025 },2026 "w2" ->2027 {2028 attached: Set(),2029 built: false,2030 expecting: false,2031 running: false,2032 session: true,2033 up: true2034 }2035 )2036}20372038[State 9]2039{2040 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2041 schedNoFence::scheduler::crashes: 2,2042 schedNoFence::scheduler::entry:2043 [{ followers: Set("c2"), leased: true, worker: "w2" }],2044 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2045 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2046 schedNoFence::scheduler::mBuild: Set(),2047 schedNoFence::scheduler::mDone: Set(),2048 schedNoFence::scheduler::mExpect: Set(),2049 schedNoFence::scheduler::mResult: Set(),2050 schedNoFence::scheduler::mRetry: Set("c1"),2051 schedNoFence::scheduler::mRevoke: Set(),2052 schedNoFence::scheduler::mSchedule: Set(),2053 schedNoFence::scheduler::published: 0,2054 schedNoFence::scheduler::publishedBy: Set(),2055 schedNoFence::scheduler::ws:2056 Map(2057 "w1" ->2058 {2059 attached: Set(),2060 built: false,2061 expecting: true,2062 running: true,2063 session: false,2064 up: true2065 },2066 "w2" ->2067 {2068 attached: Set(),2069 built: false,2070 expecting: true,2071 running: true,2072 session: true,2073 up: true2074 }2075 )2076}20772078[State 10]2079{2080 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2081 schedNoFence::scheduler::crashes: 2,2082 schedNoFence::scheduler::entry:2083 [{ followers: Set("c2"), leased: true, worker: "w2" }],2084 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2085 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2086 schedNoFence::scheduler::mBuild: Set(),2087 schedNoFence::scheduler::mDone: Set(),2088 schedNoFence::scheduler::mExpect: Set(),2089 schedNoFence::scheduler::mResult: Set(),2090 schedNoFence::scheduler::mRetry: Set("c1"),2091 schedNoFence::scheduler::mRevoke: Set(),2092 schedNoFence::scheduler::mSchedule: Set(),2093 schedNoFence::scheduler::published: 1,2094 schedNoFence::scheduler::publishedBy: Set("w1"),2095 schedNoFence::scheduler::ws:2096 Map(2097 "w1" ->2098 {2099 attached: Set(),2100 built: true,2101 expecting: false,2102 running: false,2103 session: false,2104 up: true2105 },2106 "w2" ->2107 {2108 attached: Set(),2109 built: false,2110 expecting: true,2111 running: true,2112 session: true,2113 up: true2114 }2115 )2116}21172118[State 11]2119{2120 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2121 schedNoFence::scheduler::crashes: 2,2122 schedNoFence::scheduler::entry:2123 [{ followers: Set("c2"), leased: true, worker: "w2" }],2124 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2125 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2126 schedNoFence::scheduler::mBuild: Set(),2127 schedNoFence::scheduler::mDone: Set("w2"),2128 schedNoFence::scheduler::mExpect: Set(),2129 schedNoFence::scheduler::mResult: Set(),2130 schedNoFence::scheduler::mRetry: Set("c1"),2131 schedNoFence::scheduler::mRevoke: Set(),2132 schedNoFence::scheduler::mSchedule: Set(),2133 schedNoFence::scheduler::published: 2,2134 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2135 schedNoFence::scheduler::ws:2136 Map(2137 "w1" ->2138 {2139 attached: Set(),2140 built: true,2141 expecting: false,2142 running: false,2143 session: false,2144 up: true2145 },2146 "w2" ->2147 {2148 attached: Set(),2149 built: true,2150 expecting: false,2151 running: false,2152 session: true,2153 up: true2154 }2155 )2156}21572158[violation] Found an issue (479ms at 58762 traces/second).2159Use --verbosity=3 to show executions.2160Use --seed=0x884fda3fc8903d3c --backend=rust to reproduce.2161error: Invariant violated2162An example execution:21632164[State 0]2165{2166 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2167 schedNoPush::scheduler::crashes: 0,2168 schedNoPush::scheduler::entry: [],2169 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2170 schedNoPush::scheduler::mAssigned: Set(),2171 schedNoPush::scheduler::mBuild: Set(),2172 schedNoPush::scheduler::mDone: Set(),2173 schedNoPush::scheduler::mExpect: Set(),2174 schedNoPush::scheduler::mResult: Set(),2175 schedNoPush::scheduler::mRetry: Set(),2176 schedNoPush::scheduler::mRevoke: Set(),2177 schedNoPush::scheduler::mSchedule: Set(),2178 schedNoPush::scheduler::published: 0,2179 schedNoPush::scheduler::publishedBy: Set(),2180 schedNoPush::scheduler::ws:2181 Map(2182 "w1" ->2183 {2184 attached: Set(),2185 built: false,2186 expecting: false,2187 running: false,2188 session: true,2189 up: true2190 },2191 "w2" ->2192 {2193 attached: Set(),2194 built: false,2195 expecting: false,2196 running: false,2197 session: true,2198 up: true2199 }2200 )2201}22022203[State 1]2204{2205 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2206 schedNoPush::scheduler::crashes: 0,2207 schedNoPush::scheduler::entry: [],2208 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2209 schedNoPush::scheduler::mAssigned: Set(),2210 schedNoPush::scheduler::mBuild: Set(),2211 schedNoPush::scheduler::mDone: Set(),2212 schedNoPush::scheduler::mExpect: Set(),2213 schedNoPush::scheduler::mResult: Set(),2214 schedNoPush::scheduler::mRetry: Set(),2215 schedNoPush::scheduler::mRevoke: Set(),2216 schedNoPush::scheduler::mSchedule: Set("c1"),2217 schedNoPush::scheduler::published: 0,2218 schedNoPush::scheduler::publishedBy: Set(),2219 schedNoPush::scheduler::ws:2220 Map(2221 "w1" ->2222 {2223 attached: Set(),2224 built: false,2225 expecting: false,2226 running: false,2227 session: true,2228 up: true2229 },2230 "w2" ->2231 {2232 attached: Set(),2233 built: false,2234 expecting: false,2235 running: false,2236 session: true,2237 up: true2238 }2239 )2240}22412242[State 2]2243{2244 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2245 schedNoPush::scheduler::crashes: 1,2246 schedNoPush::scheduler::entry: [],2247 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2248 schedNoPush::scheduler::mAssigned: Set(),2249 schedNoPush::scheduler::mBuild: Set(),2250 schedNoPush::scheduler::mDone: Set(),2251 schedNoPush::scheduler::mExpect: Set(),2252 schedNoPush::scheduler::mResult: Set(),2253 schedNoPush::scheduler::mRetry: Set(),2254 schedNoPush::scheduler::mRevoke: Set(),2255 schedNoPush::scheduler::mSchedule: Set("c1"),2256 schedNoPush::scheduler::published: 0,2257 schedNoPush::scheduler::publishedBy: Set(),2258 schedNoPush::scheduler::ws:2259 Map(2260 "w1" ->2261 {2262 attached: Set(),2263 built: false,2264 expecting: false,2265 running: false,2266 session: false,2267 up: false2268 },2269 "w2" ->2270 {2271 attached: Set(),2272 built: false,2273 expecting: false,2274 running: false,2275 session: true,2276 up: true2277 }2278 )2279}22802281[State 3]2282{2283 schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2284 schedNoPush::scheduler::crashes: 1,2285 schedNoPush::scheduler::entry:2286 [{ followers: Set("c1"), leased: true, worker: "w2" }],2287 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2288 schedNoPush::scheduler::mAssigned: Set(("c1", "w2")),2289 schedNoPush::scheduler::mBuild: Set(),2290 schedNoPush::scheduler::mDone: Set(),2291 schedNoPush::scheduler::mExpect: Set(),2292 schedNoPush::scheduler::mResult: Set(),2293 schedNoPush::scheduler::mRetry: Set(),2294 schedNoPush::scheduler::mRevoke: Set(),2295 schedNoPush::scheduler::mSchedule: Set(),2296 schedNoPush::scheduler::published: 0,2297 schedNoPush::scheduler::publishedBy: Set(),2298 schedNoPush::scheduler::ws:2299 Map(2300 "w1" ->2301 {2302 attached: Set(),2303 built: false,2304 expecting: false,2305 running: false,2306 session: false,2307 up: false2308 },2309 "w2" ->2310 {2311 attached: Set(),2312 built: false,2313 expecting: false,2314 running: false,2315 session: true,2316 up: true2317 }2318 )2319}23202321[State 4]2322{2323 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2324 schedNoPush::scheduler::crashes: 1,2325 schedNoPush::scheduler::entry:2326 [{ followers: Set("c1"), leased: true, worker: "w2" }],2327 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),2328 schedNoPush::scheduler::mAssigned: Set(),2329 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2330 schedNoPush::scheduler::mDone: Set(),2331 schedNoPush::scheduler::mExpect: Set(),2332 schedNoPush::scheduler::mResult: Set(),2333 schedNoPush::scheduler::mRetry: Set(),2334 schedNoPush::scheduler::mRevoke: Set(),2335 schedNoPush::scheduler::mSchedule: Set(),2336 schedNoPush::scheduler::published: 0,2337 schedNoPush::scheduler::publishedBy: Set(),2338 schedNoPush::scheduler::ws:2339 Map(2340 "w1" ->2341 {2342 attached: Set(),2343 built: false,2344 expecting: false,2345 running: false,2346 session: false,2347 up: false2348 },2349 "w2" ->2350 {2351 attached: Set(),2352 built: false,2353 expecting: false,2354 running: false,2355 session: true,2356 up: true2357 }2358 )2359}23602361[State 5]2362{2363 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2364 schedNoPush::scheduler::crashes: 2,2365 schedNoPush::scheduler::entry: [],2366 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2367 schedNoPush::scheduler::mAssigned: Set(),2368 schedNoPush::scheduler::mBuild: Set(("c1", "w2")),2369 schedNoPush::scheduler::mDone: Set(),2370 schedNoPush::scheduler::mExpect: Set(),2371 schedNoPush::scheduler::mResult: Set(),2372 schedNoPush::scheduler::mRetry: Set(),2373 schedNoPush::scheduler::mRevoke: Set(),2374 schedNoPush::scheduler::mSchedule: Set(),2375 schedNoPush::scheduler::published: 0,2376 schedNoPush::scheduler::publishedBy: Set(),2377 schedNoPush::scheduler::ws:2378 Map(2379 "w1" ->2380 {2381 attached: Set(),2382 built: false,2383 expecting: false,2384 running: false,2385 session: false,2386 up: false2387 },2388 "w2" ->2389 {2390 attached: Set(),2391 built: false,2392 expecting: false,2393 running: false,2394 session: false,2395 up: true2396 }2397 )2398}23992400[State 6]2401{2402 schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle),2403 schedNoPush::scheduler::crashes: 2,2404 schedNoPush::scheduler::entry: [],2405 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),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: true,2434 up: true2435 }2436 )2437}24382439[State 7]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(),2447 schedNoPush::scheduler::mDone: Set(),2448 schedNoPush::scheduler::mExpect: Set(),2449 schedNoPush::scheduler::mResult: Set(),2450 schedNoPush::scheduler::mRetry: Set(),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("c1"),2469 built: false,2470 expecting: true,2471 running: true,2472 session: true,2473 up: true2474 }2475 )2476}24772478[violation] Found an issue (467ms at 38544 traces/second).2479Use --verbosity=3 to show executions.2480Use --seed=0x6a7ffa0d0ad17beb --backend=rust to reproduce.2481error: Invariant violated2482An example execution:24832484[State 0]2485{2486 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2487 schedNoReport::scheduler::crashes: 0,2488 schedNoReport::scheduler::entry: [],2489 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2490 schedNoReport::scheduler::mAssigned: Set(),2491 schedNoReport::scheduler::mBuild: Set(),2492 schedNoReport::scheduler::mDone: Set(),2493 schedNoReport::scheduler::mExpect: Set(),2494 schedNoReport::scheduler::mResult: Set(),2495 schedNoReport::scheduler::mRetry: Set(),2496 schedNoReport::scheduler::mRevoke: Set(),2497 schedNoReport::scheduler::mSchedule: Set(),2498 schedNoReport::scheduler::published: 0,2499 schedNoReport::scheduler::publishedBy: Set(),2500 schedNoReport::scheduler::ws:2501 Map(2502 "w1" ->2503 {2504 attached: Set(),2505 built: false,2506 expecting: false,2507 running: false,2508 session: true,2509 up: true2510 },2511 "w2" ->2512 {2513 attached: Set(),2514 built: false,2515 expecting: false,2516 running: false,2517 session: true,2518 up: true2519 }2520 )2521}25222523[State 1]2524{2525 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2526 schedNoReport::scheduler::crashes: 1,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: false,2548 up: false2549 },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 2]2563{2564 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),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("c2"),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: false,2587 up: false2588 },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: 1,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("w2"),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: false,2627 up: false2628 },2629 "w2" ->2630 {2631 attached: Set(),2632 built: false,2633 expecting: false,2634 running: false,2635 session: true,2636 up: true2637 }2638 )2639}26402641[State 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("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: false,2743 running: false,2744 session: true,2745 up: true2746 },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("w1"),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: 1,2894 schedNoReport::scheduler::publishedBy: Set("w1"),2895 schedNoReport::scheduler::ws:2896 Map(2897 "w1" ->2898 {2899 attached: Set(),2900 built: true,2901 expecting: false,2902 running: false,2903 session: true,2904 up: true2905 },2906 "w2" ->2907 {2908 attached: Set(),2909 built: false,2910 expecting: true,2911 running: true,2912 session: false,2913 up: true2914 }2915 )2916}29172918[State 11]2919{2920 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2921 schedNoReport::scheduler::crashes: 2,2922 schedNoReport::scheduler::entry:2923 [{ followers: Set("c2"), leased: true, worker: "w1" }],2924 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2925 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2926 schedNoReport::scheduler::mBuild: Set(),2927 schedNoReport::scheduler::mDone: Set("w1"),2928 schedNoReport::scheduler::mExpect: Set(),2929 schedNoReport::scheduler::mResult: Set(),2930 schedNoReport::scheduler::mRetry: Set(),2931 schedNoReport::scheduler::mRevoke: Set(),2932 schedNoReport::scheduler::mSchedule: Set(),2933 schedNoReport::scheduler::published: 2,2934 schedNoReport::scheduler::publishedBy: Set("w1", "w2"),2935 schedNoReport::scheduler::ws:2936 Map(2937 "w1" ->2938 {2939 attached: Set(),2940 built: true,2941 expecting: false,2942 running: false,2943 session: true,2944 up: true2945 },2946 "w2" ->2947 {2948 attached: Set(),2949 built: true,2950 expecting: false,2951 running: false,2952 session: false,2953 up: true2954 }2955 )2956}29572958[violation] Found an issue (447ms at 58996 traces/second).2959Use --verbosity=3 to show executions.2960Use --seed=0x18a8b4076d8a8d74 --backend=rust to reproduce.2961error: Invariant violated2962An example execution:29632964[State 0]2965{2966 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2967 schedTerminal::scheduler::crashes: 0,2968 schedTerminal::scheduler::entry: [],2969 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),2970 schedTerminal::scheduler::mAssigned: Set(),2971 schedTerminal::scheduler::mBuild: Set(),2972 schedTerminal::scheduler::mDone: Set(),2973 schedTerminal::scheduler::mExpect: Set(),2974 schedTerminal::scheduler::mResult: Set(),2975 schedTerminal::scheduler::mRetry: Set(),2976 schedTerminal::scheduler::mRevoke: Set(),2977 schedTerminal::scheduler::mSchedule: Set(),2978 schedTerminal::scheduler::published: 0,2979 schedTerminal::scheduler::publishedBy: Set(),2980 schedTerminal::scheduler::ws:2981 Map(2982 "w1" ->2983 {2984 attached: Set(),2985 built: false,2986 expecting: false,2987 running: false,2988 session: true,2989 up: true2990 },2991 "w2" ->2992 {2993 attached: Set(),2994 built: false,2995 expecting: false,2996 running: false,2997 session: true,2998 up: true2999 }3000 )3001}30023003[State 1]3004{3005 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3006 schedTerminal::scheduler::crashes: 1,3007 schedTerminal::scheduler::entry: [],3008 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3009 schedTerminal::scheduler::mAssigned: Set(),3010 schedTerminal::scheduler::mBuild: Set(),3011 schedTerminal::scheduler::mDone: Set(),3012 schedTerminal::scheduler::mExpect: Set(),3013 schedTerminal::scheduler::mResult: Set(),3014 schedTerminal::scheduler::mRetry: Set(),3015 schedTerminal::scheduler::mRevoke: Set(),3016 schedTerminal::scheduler::mSchedule: Set(),3017 schedTerminal::scheduler::published: 0,3018 schedTerminal::scheduler::publishedBy: Set(),3019 schedTerminal::scheduler::ws:3020 Map(3021 "w1" ->3022 {3023 attached: Set(),3024 built: false,3025 expecting: false,3026 running: false,3027 session: false,3028 up: true3029 },3030 "w2" ->3031 {3032 attached: Set(),3033 built: false,3034 expecting: false,3035 running: false,3036 session: false,3037 up: true3038 }3039 )3040}30413042[State 2]3043{3044 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),3045 schedTerminal::scheduler::crashes: 1,3046 schedTerminal::scheduler::entry: [],3047 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3048 schedTerminal::scheduler::mAssigned: Set(),3049 schedTerminal::scheduler::mBuild: Set(),3050 schedTerminal::scheduler::mDone: Set(),3051 schedTerminal::scheduler::mExpect: Set(),3052 schedTerminal::scheduler::mResult: Set(),3053 schedTerminal::scheduler::mRetry: Set(),3054 schedTerminal::scheduler::mRevoke: Set(),3055 schedTerminal::scheduler::mSchedule: Set("c2"),3056 schedTerminal::scheduler::published: 0,3057 schedTerminal::scheduler::publishedBy: Set(),3058 schedTerminal::scheduler::ws:3059 Map(3060 "w1" ->3061 {3062 attached: Set(),3063 built: false,3064 expecting: false,3065 running: false,3066 session: false,3067 up: true3068 },3069 "w2" ->3070 {3071 attached: Set(),3072 built: false,3073 expecting: false,3074 running: false,3075 session: false,3076 up: true3077 }3078 )3079}30803081[State 3]3082{3083 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed),3084 schedTerminal::scheduler::crashes: 1,3085 schedTerminal::scheduler::entry: [],3086 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3087 schedTerminal::scheduler::mAssigned: Set(),3088 schedTerminal::scheduler::mBuild: Set(),3089 schedTerminal::scheduler::mDone: Set(),3090 schedTerminal::scheduler::mExpect: Set(),3091 schedTerminal::scheduler::mResult: Set(),3092 schedTerminal::scheduler::mRetry: Set(),3093 schedTerminal::scheduler::mRevoke: Set(),3094 schedTerminal::scheduler::mSchedule: Set(),3095 schedTerminal::scheduler::published: 0,3096 schedTerminal::scheduler::publishedBy: Set(),3097 schedTerminal::scheduler::ws:3098 Map(3099 "w1" ->3100 {3101 attached: Set(),3102 built: false,3103 expecting: false,3104 running: false,3105 session: false,3106 up: true3107 },3108 "w2" ->3109 {3110 attached: Set(),3111 built: false,3112 expecting: false,3113 running: false,3114 session: false,3115 up: true3116 }3117 )3118}31193120[violation] Found an issue (356ms at 5410 traces/second).3121Use --verbosity=3 to show executions.3122Use --seed=0x280d55db39d400cc --backend=rust to reproduce.3123error: Invariant violated3124An example execution:31253126[State 0]3127{3128 pushFixed::push::byPath: Map(),3129 pushFixed::push::inflight: Set(),3130 pushFixed::push::left: Map(),3131 pushFixed::push::sent: Map()3132}31333134[State 1]3135{3136 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3137 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3138 pushFixed::push::left: Map(3 -> 2),3139 pushFixed::push::sent: Map(3 -> Set("a", "b"))3140}31413142[State 2]3143{3144 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3145 pushFixed::push::inflight: Set((3, "a")),3146 pushFixed::push::left: Map(3 -> 1),3147 pushFixed::push::sent: Map(3 -> Set("a", "b"))3148}31493150[State 3]3151{3152 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3153 pushFixed::push::inflight: Set(),3154 pushFixed::push::left: Map(3 -> 0),3155 pushFixed::push::sent: Map(3 -> Set("a", "b"))3156}31573158[State 4]3159{3160 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3161 pushFixed::push::inflight: Set((2, "a"), (2, "b")),3162 pushFixed::push::left: Map(2 -> 2, 3 -> 0),3163 pushFixed::push::sent: Map(2 -> Set("a", "b"), 3 -> Set("a", "b"))3164}31653166[State 5]3167{3168 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3169 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),3170 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 0),3171 pushFixed::push::sent:3172 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3173}31743175[State 6]3176{3177 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3178 pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "b")),3179 pushFixed::push::left: Map(1 -> 2, 2 -> 1, 3 -> 0),3180 pushFixed::push::sent:3181 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3182}31833184[State 7]3185{3186 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3187 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3188 pushFixed::push::left: Map(1 -> 2, 2 -> 0, 3 -> 0),3189 pushFixed::push::sent:3190 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3191}31923193[State 8]3194{3195 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3196 pushFixed::push::inflight: Set((1, "b")),3197 pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 0),3198 pushFixed::push::sent:3199 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3200}32013202[State 9]3203{3204 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3205 pushFixed::push::inflight: Set(),3206 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3207 pushFixed::push::sent:3208 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3209}32103211[ok] No violation found (100ms at 200000 traces/second).3212Trace length statistics: max=10, min=7, average=8.103213You may increase --max-samples and --max-steps.3214Use --verbosity to produce more (or less) output.3215Use --seed=0x727076644e4f241c --backend=rust to reproduce.