nix-grpc-store-spec
checks.aarch64-linux.spec
· build #689
· raw
1tribuchet: building on eliza2An example execution:34[State 0]5{6 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),7 schedFixed::scheduler::crashes: 0,8 schedFixed::scheduler::entry: [],9 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),10 schedFixed::scheduler::mAssigned: Set(),11 schedFixed::scheduler::mBuild: Set(),12 schedFixed::scheduler::mDone: Set(),13 schedFixed::scheduler::mExpect: Set(),14 schedFixed::scheduler::mResult: Set(),15 schedFixed::scheduler::mRetry: Set(),16 schedFixed::scheduler::mRevoke: Set(),17 schedFixed::scheduler::mSchedule: Set(),18 schedFixed::scheduler::published: 0,19 schedFixed::scheduler::publishedBy: Set(),20 schedFixed::scheduler::ws:21 Map(22 "w1" ->23 {24 attached: Set(),25 built: false,26 expecting: false,27 running: false,28 session: true,29 up: true30 },31 "w2" ->32 {33 attached: Set(),34 built: false,35 expecting: false,36 running: false,37 session: true,38 up: true39 }40 )41}4243[State 1]44{45 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),46 schedFixed::scheduler::crashes: 1,47 schedFixed::scheduler::entry: [],48 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),49 schedFixed::scheduler::mAssigned: Set(),50 schedFixed::scheduler::mBuild: Set(),51 schedFixed::scheduler::mDone: Set(),52 schedFixed::scheduler::mExpect: Set(),53 schedFixed::scheduler::mResult: Set(),54 schedFixed::scheduler::mRetry: Set(),55 schedFixed::scheduler::mRevoke: Set(),56 schedFixed::scheduler::mSchedule: Set(),57 schedFixed::scheduler::published: 0,58 schedFixed::scheduler::publishedBy: Set(),59 schedFixed::scheduler::ws:60 Map(61 "w1" ->62 {63 attached: Set(),64 built: false,65 expecting: false,66 running: false,67 session: false,68 up: false69 },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" -> 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: true,116 up: true117 }118 )119}120121[State 3]122{123 schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),124 schedFixed::scheduler::crashes: 2,125 schedFixed::scheduler::entry: [],126 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),127 schedFixed::scheduler::mAssigned: Set(),128 schedFixed::scheduler::mBuild: Set(),129 schedFixed::scheduler::mDone: Set(),130 schedFixed::scheduler::mExpect: Set(),131 schedFixed::scheduler::mResult: Set(),132 schedFixed::scheduler::mRetry: Set(),133 schedFixed::scheduler::mRevoke: Set(),134 schedFixed::scheduler::mSchedule: Set(),135 schedFixed::scheduler::published: 0,136 schedFixed::scheduler::publishedBy: Set(),137 schedFixed::scheduler::ws:138 Map(139 "w1" ->140 {141 attached: Set(),142 built: false,143 expecting: false,144 running: false,145 session: false,146 up: true147 },148 "w2" ->149 {150 attached: Set(),151 built: false,152 expecting: false,153 running: false,154 session: false,155 up: true156 }157 )158}159160[State 4]161{162 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),163 schedFixed::scheduler::crashes: 2,164 schedFixed::scheduler::entry: [],165 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),166 schedFixed::scheduler::mAssigned: Set(),167 schedFixed::scheduler::mBuild: Set(),168 schedFixed::scheduler::mDone: Set(),169 schedFixed::scheduler::mExpect: Set(),170 schedFixed::scheduler::mResult: Set(),171 schedFixed::scheduler::mRetry: Set(),172 schedFixed::scheduler::mRevoke: Set(),173 schedFixed::scheduler::mSchedule: Set("c1"),174 schedFixed::scheduler::published: 0,175 schedFixed::scheduler::publishedBy: Set(),176 schedFixed::scheduler::ws:177 Map(178 "w1" ->179 {180 attached: Set(),181 built: false,182 expecting: false,183 running: false,184 session: false,185 up: true186 },187 "w2" ->188 {189 attached: Set(),190 built: false,191 expecting: false,192 running: false,193 session: false,194 up: true195 }196 )197}198199[State 5]200{201 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> 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(),211 schedFixed::scheduler::mRevoke: Set(),212 schedFixed::scheduler::mSchedule: Set("c1", "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(),250 schedFixed::scheduler::mRevoke: Set(),251 schedFixed::scheduler::mSchedule: Set("c1", "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: true,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: true,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: true,391 up: true392 }393 )394}395396[State 10]397{398 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),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(("c1", "w1")),404 schedFixed::scheduler::mBuild: Set(("c2", "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: true,431 up: true432 }433 )434}435436[State 11]437{438 schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),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(("c1", "w1")),444 schedFixed::scheduler::mBuild: Set(),445 schedFixed::scheduler::mDone: Set(),446 schedFixed::scheduler::mExpect: Set("w1"),447 schedFixed::scheduler::mResult: Set(),448 schedFixed::scheduler::mRetry: Set("c2"),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" -> CQueued, "c2" -> CQueued),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(("c1", "w1")),484 schedFixed::scheduler::mBuild: Set(),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("c2"),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" -> CQueued, "c2" -> CQueued),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(("c1", "w1"), ("c2", "w1")),524 schedFixed::scheduler::mBuild: Set(),525 schedFixed::scheduler::mDone: Set(),526 schedFixed::scheduler::mExpect: Set("w1"),527 schedFixed::scheduler::mResult: Set(),528 schedFixed::scheduler::mRetry: Set(),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" -> CQueued, "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(("c1", "w1")),564 schedFixed::scheduler::mBuild: Set(("c2", "w1")),565 schedFixed::scheduler::mDone: Set(),566 schedFixed::scheduler::mExpect: Set("w1"),567 schedFixed::scheduler::mResult: Set(),568 schedFixed::scheduler::mRetry: Set(),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(("c1", "w1")),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(),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" -> CSent("w1"), "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(),644 schedFixed::scheduler::mBuild: Set(("c1", "w1")),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(),685 schedFixed::scheduler::mDone: Set(),686 schedFixed::scheduler::mExpect: Set("w1"),687 schedFixed::scheduler::mResult: Set(),688 schedFixed::scheduler::mRetry: Set("c1", "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(),725 schedFixed::scheduler::mDone: Set(),726 schedFixed::scheduler::mExpect: Set("w1"),727 schedFixed::scheduler::mResult: Set(),728 schedFixed::scheduler::mRetry: Set("c1"),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" -> CQueued, "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(),769 schedFixed::scheduler::mRevoke: Set(),770 schedFixed::scheduler::mSchedule: Set("c1", "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(("c1", "w1")),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("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"), ("c2", "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(),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(("c2", "w1")),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(),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(),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: true,940 running: true,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" -> CQueued),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(("c2", "w1")),964 schedFixed::scheduler::mBuild: Set(),965 schedFixed::scheduler::mDone: Set(),966 schedFixed::scheduler::mExpect: Set(),967 schedFixed::scheduler::mResult: Set(),968 schedFixed::scheduler::mRetry: Set(),969 schedFixed::scheduler::mRevoke: Set(),970 schedFixed::scheduler::mSchedule: Set(),971 schedFixed::scheduler::published: 0,972 schedFixed::scheduler::publishedBy: Set(),973 schedFixed::scheduler::ws:974 Map(975 "w1" ->976 {977 attached: Set("c1"),978 built: false,979 expecting: true,980 running: true,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(),1007 schedFixed::scheduler::mResult: Set(),1008 schedFixed::scheduler::mRetry: Set(),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("c1"),1018 built: false,1019 expecting: true,1020 running: true,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" -> CSent("w1"), "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("w1"),1046 schedFixed::scheduler::mExpect: Set(),1047 schedFixed::scheduler::mResult: Set("c1"),1048 schedFixed::scheduler::mRetry: Set(),1049 schedFixed::scheduler::mRevoke: Set(),1050 schedFixed::scheduler::mSchedule: Set(),1051 schedFixed::scheduler::published: 1,1052 schedFixed::scheduler::publishedBy: Set("w1"),1053 schedFixed::scheduler::ws:1054 Map(1055 "w1" ->1056 {1057 attached: Set(),1058 built: true,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" -> CDone, "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("w1"),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(),1091 schedFixed::scheduler::published: 1,1092 schedFixed::scheduler::publishedBy: Set("w1"),1093 schedFixed::scheduler::ws:1094 Map(1095 "w1" ->1096 {1097 attached: Set(),1098 built: true,1099 expecting: false,1100 running: false,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" -> CDone, "c2" -> CSent("w1")),1119 schedFixed::scheduler::crashes: 2,1120 schedFixed::scheduler::entry: [],1121 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1122 schedFixed::scheduler::mAssigned: Set(),1123 schedFixed::scheduler::mBuild: Set(("c2", "w1")),1124 schedFixed::scheduler::mDone: Set(),1125 schedFixed::scheduler::mExpect: Set(),1126 schedFixed::scheduler::mResult: Set(),1127 schedFixed::scheduler::mRetry: Set(),1128 schedFixed::scheduler::mRevoke: Set(),1129 schedFixed::scheduler::mSchedule: Set(),1130 schedFixed::scheduler::published: 1,1131 schedFixed::scheduler::publishedBy: Set("w1"),1132 schedFixed::scheduler::ws:1133 Map(1134 "w1" ->1135 {1136 attached: Set(),1137 built: true,1138 expecting: false,1139 running: false,1140 session: true,1141 up: true1142 },1143 "w2" ->1144 {1145 attached: Set(),1146 built: false,1147 expecting: false,1148 running: false,1149 session: true,1150 up: true1151 }1152 )1153}11541155[State 29]1156{1157 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CSent("w1")),1158 schedFixed::scheduler::crashes: 2,1159 schedFixed::scheduler::entry: [],1160 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1161 schedFixed::scheduler::mAssigned: Set(),1162 schedFixed::scheduler::mBuild: Set(),1163 schedFixed::scheduler::mDone: Set(),1164 schedFixed::scheduler::mExpect: Set(),1165 schedFixed::scheduler::mResult: Set("c2"),1166 schedFixed::scheduler::mRetry: Set(),1167 schedFixed::scheduler::mRevoke: Set(),1168 schedFixed::scheduler::mSchedule: Set(),1169 schedFixed::scheduler::published: 1,1170 schedFixed::scheduler::publishedBy: Set("w1"),1171 schedFixed::scheduler::ws:1172 Map(1173 "w1" ->1174 {1175 attached: Set(),1176 built: true,1177 expecting: false,1178 running: false,1179 session: true,1180 up: true1181 },1182 "w2" ->1183 {1184 attached: Set(),1185 built: false,1186 expecting: false,1187 running: false,1188 session: true,1189 up: true1190 }1191 )1192}11931194[State 30]1195{1196 schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),1197 schedFixed::scheduler::crashes: 2,1198 schedFixed::scheduler::entry: [],1199 schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),1200 schedFixed::scheduler::mAssigned: Set(),1201 schedFixed::scheduler::mBuild: Set(),1202 schedFixed::scheduler::mDone: Set(),1203 schedFixed::scheduler::mExpect: Set(),1204 schedFixed::scheduler::mResult: Set(),1205 schedFixed::scheduler::mRetry: Set(),1206 schedFixed::scheduler::mRevoke: Set(),1207 schedFixed::scheduler::mSchedule: Set(),1208 schedFixed::scheduler::published: 1,1209 schedFixed::scheduler::publishedBy: Set("w1"),1210 schedFixed::scheduler::ws:1211 Map(1212 "w1" ->1213 {1214 attached: Set(),1215 built: true,1216 expecting: false,1217 running: false,1218 session: true,1219 up: true1220 },1221 "w2" ->1222 {1223 attached: Set(),1224 built: false,1225 expecting: false,1226 running: false,1227 session: true,1228 up: true1229 }1230 )1231}12321233[ok] No violation found (2331ms at 12870 traces/second).1234Trace length statistics: max=29, min=16, average=19.141235You may increase --max-samples and --max-steps.1236Use --verbosity to produce more (or less) output.1237Use --seed=0x67454b30907f82f5 --backend=rust to reproduce.1238An example execution:12391240[State 0]1241{1242 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1243 schedNoRevoke::scheduler::crashes: 0,1244 schedNoRevoke::scheduler::entry: [],1245 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1246 schedNoRevoke::scheduler::mAssigned: Set(),1247 schedNoRevoke::scheduler::mBuild: Set(),1248 schedNoRevoke::scheduler::mDone: Set(),1249 schedNoRevoke::scheduler::mExpect: Set(),1250 schedNoRevoke::scheduler::mResult: Set(),1251 schedNoRevoke::scheduler::mRetry: Set(),1252 schedNoRevoke::scheduler::mRevoke: Set(),1253 schedNoRevoke::scheduler::mSchedule: Set(),1254 schedNoRevoke::scheduler::published: 0,1255 schedNoRevoke::scheduler::publishedBy: Set(),1256 schedNoRevoke::scheduler::ws:1257 Map(1258 "w1" ->1259 {1260 attached: Set(),1261 built: false,1262 expecting: false,1263 running: false,1264 session: true,1265 up: true1266 },1267 "w2" ->1268 {1269 attached: Set(),1270 built: false,1271 expecting: false,1272 running: false,1273 session: true,1274 up: true1275 }1276 )1277}12781279[State 1]1280{1281 schedNoRevoke::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1282 schedNoRevoke::scheduler::crashes: 1,1283 schedNoRevoke::scheduler::entry: [],1284 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1285 schedNoRevoke::scheduler::mAssigned: Set(),1286 schedNoRevoke::scheduler::mBuild: Set(),1287 schedNoRevoke::scheduler::mDone: Set(),1288 schedNoRevoke::scheduler::mExpect: Set(),1289 schedNoRevoke::scheduler::mResult: Set(),1290 schedNoRevoke::scheduler::mRetry: Set(),1291 schedNoRevoke::scheduler::mRevoke: Set(),1292 schedNoRevoke::scheduler::mSchedule: Set(),1293 schedNoRevoke::scheduler::published: 0,1294 schedNoRevoke::scheduler::publishedBy: Set(),1295 schedNoRevoke::scheduler::ws:1296 Map(1297 "w1" ->1298 {1299 attached: Set(),1300 built: false,1301 expecting: false,1302 running: false,1303 session: false,1304 up: false1305 },1306 "w2" ->1307 {1308 attached: Set(),1309 built: false,1310 expecting: false,1311 running: false,1312 session: true,1313 up: true1314 }1315 )1316}13171318[State 2]1319{1320 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1321 schedNoRevoke::scheduler::crashes: 1,1322 schedNoRevoke::scheduler::entry: [],1323 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1324 schedNoRevoke::scheduler::mAssigned: Set(),1325 schedNoRevoke::scheduler::mBuild: Set(),1326 schedNoRevoke::scheduler::mDone: Set(),1327 schedNoRevoke::scheduler::mExpect: Set(),1328 schedNoRevoke::scheduler::mResult: Set(),1329 schedNoRevoke::scheduler::mRetry: Set(),1330 schedNoRevoke::scheduler::mRevoke: Set(),1331 schedNoRevoke::scheduler::mSchedule: Set("c1"),1332 schedNoRevoke::scheduler::published: 0,1333 schedNoRevoke::scheduler::publishedBy: Set(),1334 schedNoRevoke::scheduler::ws:1335 Map(1336 "w1" ->1337 {1338 attached: Set(),1339 built: false,1340 expecting: false,1341 running: false,1342 session: false,1343 up: false1344 },1345 "w2" ->1346 {1347 attached: Set(),1348 built: false,1349 expecting: false,1350 running: false,1351 session: true,1352 up: true1353 }1354 )1355}13561357[State 3]1358{1359 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1360 schedNoRevoke::scheduler::crashes: 1,1361 schedNoRevoke::scheduler::entry:1362 [{ followers: Set("c1"), leased: true, worker: "w2" }],1363 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1364 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1365 schedNoRevoke::scheduler::mBuild: Set(),1366 schedNoRevoke::scheduler::mDone: Set(),1367 schedNoRevoke::scheduler::mExpect: Set("w2"),1368 schedNoRevoke::scheduler::mResult: Set(),1369 schedNoRevoke::scheduler::mRetry: Set(),1370 schedNoRevoke::scheduler::mRevoke: Set(),1371 schedNoRevoke::scheduler::mSchedule: Set(),1372 schedNoRevoke::scheduler::published: 0,1373 schedNoRevoke::scheduler::publishedBy: Set(),1374 schedNoRevoke::scheduler::ws:1375 Map(1376 "w1" ->1377 {1378 attached: Set(),1379 built: false,1380 expecting: false,1381 running: false,1382 session: false,1383 up: false1384 },1385 "w2" ->1386 {1387 attached: Set(),1388 built: false,1389 expecting: false,1390 running: false,1391 session: true,1392 up: true1393 }1394 )1395}13961397[State 4]1398{1399 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1400 schedNoRevoke::scheduler::crashes: 1,1401 schedNoRevoke::scheduler::entry:1402 [{ followers: Set("c1"), leased: true, worker: "w2" }],1403 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 0),1404 schedNoRevoke::scheduler::mAssigned: Set(("c1", "w2")),1405 schedNoRevoke::scheduler::mBuild: Set(),1406 schedNoRevoke::scheduler::mDone: Set(),1407 schedNoRevoke::scheduler::mExpect: Set(),1408 schedNoRevoke::scheduler::mResult: Set(),1409 schedNoRevoke::scheduler::mRetry: Set(),1410 schedNoRevoke::scheduler::mRevoke: Set(),1411 schedNoRevoke::scheduler::mSchedule: Set(),1412 schedNoRevoke::scheduler::published: 0,1413 schedNoRevoke::scheduler::publishedBy: Set(),1414 schedNoRevoke::scheduler::ws:1415 Map(1416 "w1" ->1417 {1418 attached: Set(),1419 built: false,1420 expecting: false,1421 running: false,1422 session: false,1423 up: false1424 },1425 "w2" ->1426 {1427 attached: Set(),1428 built: false,1429 expecting: true,1430 running: true,1431 session: true,1432 up: true1433 }1434 )1435}14361437[State 5]1438{1439 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1440 schedNoRevoke::scheduler::crashes: 2,1441 schedNoRevoke::scheduler::entry: [],1442 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1443 schedNoRevoke::scheduler::mAssigned: Set(),1444 schedNoRevoke::scheduler::mBuild: Set(),1445 schedNoRevoke::scheduler::mDone: Set(),1446 schedNoRevoke::scheduler::mExpect: Set(),1447 schedNoRevoke::scheduler::mResult: Set(),1448 schedNoRevoke::scheduler::mRetry: Set("c1"),1449 schedNoRevoke::scheduler::mRevoke: Set(),1450 schedNoRevoke::scheduler::mSchedule: Set(),1451 schedNoRevoke::scheduler::published: 0,1452 schedNoRevoke::scheduler::publishedBy: Set(),1453 schedNoRevoke::scheduler::ws:1454 Map(1455 "w1" ->1456 {1457 attached: Set(),1458 built: false,1459 expecting: false,1460 running: false,1461 session: false,1462 up: false1463 },1464 "w2" ->1465 {1466 attached: Set(),1467 built: false,1468 expecting: true,1469 running: true,1470 session: false,1471 up: true1472 }1473 )1474}14751476[State 6]1477{1478 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1479 schedNoRevoke::scheduler::crashes: 2,1480 schedNoRevoke::scheduler::entry: [],1481 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1482 schedNoRevoke::scheduler::mAssigned: Set(),1483 schedNoRevoke::scheduler::mBuild: Set(),1484 schedNoRevoke::scheduler::mDone: Set(),1485 schedNoRevoke::scheduler::mExpect: Set(),1486 schedNoRevoke::scheduler::mResult: Set(),1487 schedNoRevoke::scheduler::mRetry: Set("c1"),1488 schedNoRevoke::scheduler::mRevoke: Set(),1489 schedNoRevoke::scheduler::mSchedule: Set("c2"),1490 schedNoRevoke::scheduler::published: 0,1491 schedNoRevoke::scheduler::publishedBy: Set(),1492 schedNoRevoke::scheduler::ws:1493 Map(1494 "w1" ->1495 {1496 attached: Set(),1497 built: false,1498 expecting: false,1499 running: false,1500 session: false,1501 up: false1502 },1503 "w2" ->1504 {1505 attached: Set(),1506 built: false,1507 expecting: true,1508 running: true,1509 session: false,1510 up: true1511 }1512 )1513}15141515[State 7]1516{1517 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1518 schedNoRevoke::scheduler::crashes: 2,1519 schedNoRevoke::scheduler::entry: [],1520 schedNoRevoke::scheduler::free: Map("w1" -> 1, "w2" -> 1),1521 schedNoRevoke::scheduler::mAssigned: Set(),1522 schedNoRevoke::scheduler::mBuild: Set(),1523 schedNoRevoke::scheduler::mDone: Set(),1524 schedNoRevoke::scheduler::mExpect: Set(),1525 schedNoRevoke::scheduler::mResult: Set(),1526 schedNoRevoke::scheduler::mRetry: Set("c1"),1527 schedNoRevoke::scheduler::mRevoke: Set(),1528 schedNoRevoke::scheduler::mSchedule: Set("c2"),1529 schedNoRevoke::scheduler::published: 0,1530 schedNoRevoke::scheduler::publishedBy: Set(),1531 schedNoRevoke::scheduler::ws:1532 Map(1533 "w1" ->1534 {1535 attached: Set(),1536 built: false,1537 expecting: false,1538 running: false,1539 session: true,1540 up: true1541 },1542 "w2" ->1543 {1544 attached: Set(),1545 built: false,1546 expecting: true,1547 running: true,1548 session: false,1549 up: true1550 }1551 )1552}15531554[State 8]1555{1556 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1557 schedNoRevoke::scheduler::crashes: 2,1558 schedNoRevoke::scheduler::entry:1559 [{ followers: Set("c2"), leased: true, worker: "w1" }],1560 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1561 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1562 schedNoRevoke::scheduler::mBuild: Set(),1563 schedNoRevoke::scheduler::mDone: Set(),1564 schedNoRevoke::scheduler::mExpect: Set("w1"),1565 schedNoRevoke::scheduler::mResult: Set(),1566 schedNoRevoke::scheduler::mRetry: Set("c1"),1567 schedNoRevoke::scheduler::mRevoke: Set(),1568 schedNoRevoke::scheduler::mSchedule: Set(),1569 schedNoRevoke::scheduler::published: 0,1570 schedNoRevoke::scheduler::publishedBy: Set(),1571 schedNoRevoke::scheduler::ws:1572 Map(1573 "w1" ->1574 {1575 attached: Set(),1576 built: false,1577 expecting: false,1578 running: false,1579 session: true,1580 up: true1581 },1582 "w2" ->1583 {1584 attached: Set(),1585 built: false,1586 expecting: true,1587 running: true,1588 session: false,1589 up: true1590 }1591 )1592}15931594[State 9]1595{1596 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1597 schedNoRevoke::scheduler::crashes: 2,1598 schedNoRevoke::scheduler::entry:1599 [{ followers: Set("c2"), leased: true, worker: "w1" }],1600 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 1),1601 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1602 schedNoRevoke::scheduler::mBuild: Set(),1603 schedNoRevoke::scheduler::mDone: Set(),1604 schedNoRevoke::scheduler::mExpect: Set(),1605 schedNoRevoke::scheduler::mResult: Set(),1606 schedNoRevoke::scheduler::mRetry: Set("c1"),1607 schedNoRevoke::scheduler::mRevoke: Set(),1608 schedNoRevoke::scheduler::mSchedule: Set(),1609 schedNoRevoke::scheduler::published: 0,1610 schedNoRevoke::scheduler::publishedBy: Set(),1611 schedNoRevoke::scheduler::ws:1612 Map(1613 "w1" ->1614 {1615 attached: Set(),1616 built: false,1617 expecting: true,1618 running: true,1619 session: true,1620 up: true1621 },1622 "w2" ->1623 {1624 attached: Set(),1625 built: false,1626 expecting: true,1627 running: true,1628 session: false,1629 up: true1630 }1631 )1632}16331634[State 10]1635{1636 schedNoRevoke::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1637 schedNoRevoke::scheduler::crashes: 2,1638 schedNoRevoke::scheduler::entry:1639 [{ followers: Set("c2"), leased: true, worker: "w1" }],1640 schedNoRevoke::scheduler::free: Map("w1" -> 0, "w2" -> 0),1641 schedNoRevoke::scheduler::mAssigned: Set(("c2", "w1")),1642 schedNoRevoke::scheduler::mBuild: Set(),1643 schedNoRevoke::scheduler::mDone: Set(),1644 schedNoRevoke::scheduler::mExpect: Set(),1645 schedNoRevoke::scheduler::mResult: Set(),1646 schedNoRevoke::scheduler::mRetry: Set("c1"),1647 schedNoRevoke::scheduler::mRevoke: Set(),1648 schedNoRevoke::scheduler::mSchedule: Set(),1649 schedNoRevoke::scheduler::published: 0,1650 schedNoRevoke::scheduler::publishedBy: Set(),1651 schedNoRevoke::scheduler::ws:1652 Map(1653 "w1" ->1654 {1655 attached: Set(),1656 built: false,1657 expecting: true,1658 running: true,1659 session: true,1660 up: true1661 },1662 "w2" ->1663 {1664 attached: Set(),1665 built: false,1666 expecting: true,1667 running: true,1668 session: true,1669 up: true1670 }1671 )1672}16731674[violation] Found an issue (2895ms at 9886 traces/second).1675Use --verbosity=3 to show executions.1676Use --seed=0xde8ac1580b890e0c --backend=rust to reproduce.1677error: Invariant violated1678An example execution:16791680[State 0]1681{1682 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1683 schedNoFence::scheduler::crashes: 0,1684 schedNoFence::scheduler::entry: [],1685 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1686 schedNoFence::scheduler::mAssigned: Set(),1687 schedNoFence::scheduler::mBuild: Set(),1688 schedNoFence::scheduler::mDone: Set(),1689 schedNoFence::scheduler::mExpect: Set(),1690 schedNoFence::scheduler::mResult: Set(),1691 schedNoFence::scheduler::mRetry: Set(),1692 schedNoFence::scheduler::mRevoke: Set(),1693 schedNoFence::scheduler::mSchedule: Set(),1694 schedNoFence::scheduler::published: 0,1695 schedNoFence::scheduler::publishedBy: Set(),1696 schedNoFence::scheduler::ws:1697 Map(1698 "w1" ->1699 {1700 attached: Set(),1701 built: false,1702 expecting: false,1703 running: false,1704 session: true,1705 up: true1706 },1707 "w2" ->1708 {1709 attached: Set(),1710 built: false,1711 expecting: false,1712 running: false,1713 session: true,1714 up: true1715 }1716 )1717}17181719[State 1]1720{1721 schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),1722 schedNoFence::scheduler::crashes: 1,1723 schedNoFence::scheduler::entry: [],1724 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1725 schedNoFence::scheduler::mAssigned: Set(),1726 schedNoFence::scheduler::mBuild: Set(),1727 schedNoFence::scheduler::mDone: Set(),1728 schedNoFence::scheduler::mExpect: Set(),1729 schedNoFence::scheduler::mResult: Set(),1730 schedNoFence::scheduler::mRetry: Set(),1731 schedNoFence::scheduler::mRevoke: Set(),1732 schedNoFence::scheduler::mSchedule: Set(),1733 schedNoFence::scheduler::published: 0,1734 schedNoFence::scheduler::publishedBy: Set(),1735 schedNoFence::scheduler::ws:1736 Map(1737 "w1" ->1738 {1739 attached: Set(),1740 built: false,1741 expecting: false,1742 running: false,1743 session: true,1744 up: true1745 },1746 "w2" ->1747 {1748 attached: Set(),1749 built: false,1750 expecting: false,1751 running: false,1752 session: false,1753 up: false1754 }1755 )1756}17571758[State 2]1759{1760 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1761 schedNoFence::scheduler::crashes: 1,1762 schedNoFence::scheduler::entry: [],1763 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1764 schedNoFence::scheduler::mAssigned: Set(),1765 schedNoFence::scheduler::mBuild: Set(),1766 schedNoFence::scheduler::mDone: Set(),1767 schedNoFence::scheduler::mExpect: Set(),1768 schedNoFence::scheduler::mResult: Set(),1769 schedNoFence::scheduler::mRetry: Set(),1770 schedNoFence::scheduler::mRevoke: Set(),1771 schedNoFence::scheduler::mSchedule: Set("c1"),1772 schedNoFence::scheduler::published: 0,1773 schedNoFence::scheduler::publishedBy: Set(),1774 schedNoFence::scheduler::ws:1775 Map(1776 "w1" ->1777 {1778 attached: Set(),1779 built: false,1780 expecting: false,1781 running: false,1782 session: true,1783 up: true1784 },1785 "w2" ->1786 {1787 attached: Set(),1788 built: false,1789 expecting: false,1790 running: false,1791 session: false,1792 up: false1793 }1794 )1795}17961797[State 3]1798{1799 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1800 schedNoFence::scheduler::crashes: 1,1801 schedNoFence::scheduler::entry:1802 [{ followers: Set("c1"), leased: true, worker: "w1" }],1803 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1804 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1805 schedNoFence::scheduler::mBuild: Set(),1806 schedNoFence::scheduler::mDone: Set(),1807 schedNoFence::scheduler::mExpect: Set("w1"),1808 schedNoFence::scheduler::mResult: Set(),1809 schedNoFence::scheduler::mRetry: Set(),1810 schedNoFence::scheduler::mRevoke: Set(),1811 schedNoFence::scheduler::mSchedule: Set(),1812 schedNoFence::scheduler::published: 0,1813 schedNoFence::scheduler::publishedBy: Set(),1814 schedNoFence::scheduler::ws:1815 Map(1816 "w1" ->1817 {1818 attached: Set(),1819 built: false,1820 expecting: false,1821 running: false,1822 session: true,1823 up: true1824 },1825 "w2" ->1826 {1827 attached: Set(),1828 built: false,1829 expecting: false,1830 running: false,1831 session: false,1832 up: false1833 }1834 )1835}18361837[State 4]1838{1839 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1840 schedNoFence::scheduler::crashes: 1,1841 schedNoFence::scheduler::entry:1842 [{ followers: Set("c1"), leased: true, worker: "w1" }],1843 schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),1844 schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),1845 schedNoFence::scheduler::mBuild: Set(),1846 schedNoFence::scheduler::mDone: Set(),1847 schedNoFence::scheduler::mExpect: Set(),1848 schedNoFence::scheduler::mResult: Set(),1849 schedNoFence::scheduler::mRetry: Set(),1850 schedNoFence::scheduler::mRevoke: Set(),1851 schedNoFence::scheduler::mSchedule: Set(),1852 schedNoFence::scheduler::published: 0,1853 schedNoFence::scheduler::publishedBy: Set(),1854 schedNoFence::scheduler::ws:1855 Map(1856 "w1" ->1857 {1858 attached: Set(),1859 built: false,1860 expecting: true,1861 running: true,1862 session: true,1863 up: true1864 },1865 "w2" ->1866 {1867 attached: Set(),1868 built: false,1869 expecting: false,1870 running: false,1871 session: false,1872 up: false1873 }1874 )1875}18761877[State 5]1878{1879 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),1880 schedNoFence::scheduler::crashes: 2,1881 schedNoFence::scheduler::entry: [],1882 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1883 schedNoFence::scheduler::mAssigned: Set(),1884 schedNoFence::scheduler::mBuild: Set(),1885 schedNoFence::scheduler::mDone: Set(),1886 schedNoFence::scheduler::mExpect: Set(),1887 schedNoFence::scheduler::mResult: Set(),1888 schedNoFence::scheduler::mRetry: Set("c1"),1889 schedNoFence::scheduler::mRevoke: Set(),1890 schedNoFence::scheduler::mSchedule: Set(),1891 schedNoFence::scheduler::published: 0,1892 schedNoFence::scheduler::publishedBy: Set(),1893 schedNoFence::scheduler::ws:1894 Map(1895 "w1" ->1896 {1897 attached: Set(),1898 built: false,1899 expecting: true,1900 running: true,1901 session: false,1902 up: true1903 },1904 "w2" ->1905 {1906 attached: Set(),1907 built: false,1908 expecting: false,1909 running: false,1910 session: false,1911 up: false1912 }1913 )1914}19151916[State 6]1917{1918 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1919 schedNoFence::scheduler::crashes: 2,1920 schedNoFence::scheduler::entry: [],1921 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1922 schedNoFence::scheduler::mAssigned: Set(),1923 schedNoFence::scheduler::mBuild: Set(),1924 schedNoFence::scheduler::mDone: Set(),1925 schedNoFence::scheduler::mExpect: Set(),1926 schedNoFence::scheduler::mResult: Set(),1927 schedNoFence::scheduler::mRetry: Set("c1"),1928 schedNoFence::scheduler::mRevoke: Set(),1929 schedNoFence::scheduler::mSchedule: Set("c2"),1930 schedNoFence::scheduler::published: 0,1931 schedNoFence::scheduler::publishedBy: Set(),1932 schedNoFence::scheduler::ws:1933 Map(1934 "w1" ->1935 {1936 attached: Set(),1937 built: false,1938 expecting: true,1939 running: true,1940 session: false,1941 up: true1942 },1943 "w2" ->1944 {1945 attached: Set(),1946 built: false,1947 expecting: false,1948 running: false,1949 session: false,1950 up: false1951 }1952 )1953}19541955[State 7]1956{1957 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1958 schedNoFence::scheduler::crashes: 2,1959 schedNoFence::scheduler::entry: [],1960 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),1961 schedNoFence::scheduler::mAssigned: Set(),1962 schedNoFence::scheduler::mBuild: Set(),1963 schedNoFence::scheduler::mDone: Set(),1964 schedNoFence::scheduler::mExpect: Set(),1965 schedNoFence::scheduler::mResult: Set(),1966 schedNoFence::scheduler::mRetry: Set(),1967 schedNoFence::scheduler::mRevoke: Set(),1968 schedNoFence::scheduler::mSchedule: Set("c1", "c2"),1969 schedNoFence::scheduler::published: 0,1970 schedNoFence::scheduler::publishedBy: Set(),1971 schedNoFence::scheduler::ws:1972 Map(1973 "w1" ->1974 {1975 attached: Set(),1976 built: false,1977 expecting: true,1978 running: true,1979 session: false,1980 up: true1981 },1982 "w2" ->1983 {1984 attached: Set(),1985 built: false,1986 expecting: false,1987 running: false,1988 session: false,1989 up: false1990 }1991 )1992}19931994[State 8]1995{1996 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),1997 schedNoFence::scheduler::crashes: 2,1998 schedNoFence::scheduler::entry: [],1999 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),2000 schedNoFence::scheduler::mAssigned: Set(),2001 schedNoFence::scheduler::mBuild: Set(),2002 schedNoFence::scheduler::mDone: Set(),2003 schedNoFence::scheduler::mExpect: Set(),2004 schedNoFence::scheduler::mResult: Set(),2005 schedNoFence::scheduler::mRetry: Set(),2006 schedNoFence::scheduler::mRevoke: Set(),2007 schedNoFence::scheduler::mSchedule: Set("c1", "c2"),2008 schedNoFence::scheduler::published: 0,2009 schedNoFence::scheduler::publishedBy: Set(),2010 schedNoFence::scheduler::ws:2011 Map(2012 "w1" ->2013 {2014 attached: Set(),2015 built: false,2016 expecting: true,2017 running: true,2018 session: false,2019 up: true2020 },2021 "w2" ->2022 {2023 attached: Set(),2024 built: false,2025 expecting: false,2026 running: false,2027 session: true,2028 up: true2029 }2030 )2031}20322033[State 9]2034{2035 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2036 schedNoFence::scheduler::crashes: 2,2037 schedNoFence::scheduler::entry:2038 [{ followers: Set("c2"), leased: true, worker: "w2" }],2039 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2040 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2041 schedNoFence::scheduler::mBuild: Set(),2042 schedNoFence::scheduler::mDone: Set(),2043 schedNoFence::scheduler::mExpect: Set("w2"),2044 schedNoFence::scheduler::mResult: Set(),2045 schedNoFence::scheduler::mRetry: Set(),2046 schedNoFence::scheduler::mRevoke: Set(),2047 schedNoFence::scheduler::mSchedule: Set("c1"),2048 schedNoFence::scheduler::published: 0,2049 schedNoFence::scheduler::publishedBy: Set(),2050 schedNoFence::scheduler::ws:2051 Map(2052 "w1" ->2053 {2054 attached: Set(),2055 built: false,2056 expecting: true,2057 running: true,2058 session: false,2059 up: true2060 },2061 "w2" ->2062 {2063 attached: Set(),2064 built: false,2065 expecting: false,2066 running: false,2067 session: true,2068 up: true2069 }2070 )2071}20722073[State 10]2074{2075 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2076 schedNoFence::scheduler::crashes: 2,2077 schedNoFence::scheduler::entry:2078 [{ followers: Set("c2"), leased: true, worker: "w2" }],2079 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2080 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2081 schedNoFence::scheduler::mBuild: Set(),2082 schedNoFence::scheduler::mDone: Set(),2083 schedNoFence::scheduler::mExpect: Set(),2084 schedNoFence::scheduler::mResult: Set(),2085 schedNoFence::scheduler::mRetry: Set(),2086 schedNoFence::scheduler::mRevoke: Set(),2087 schedNoFence::scheduler::mSchedule: Set("c1"),2088 schedNoFence::scheduler::published: 0,2089 schedNoFence::scheduler::publishedBy: Set(),2090 schedNoFence::scheduler::ws:2091 Map(2092 "w1" ->2093 {2094 attached: Set(),2095 built: false,2096 expecting: true,2097 running: true,2098 session: false,2099 up: true2100 },2101 "w2" ->2102 {2103 attached: Set(),2104 built: false,2105 expecting: true,2106 running: true,2107 session: true,2108 up: true2109 }2110 )2111}21122113[State 11]2114{2115 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2116 schedNoFence::scheduler::crashes: 2,2117 schedNoFence::scheduler::entry:2118 [{ followers: Set("c2"), leased: true, worker: "w2" }],2119 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2120 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2121 schedNoFence::scheduler::mBuild: Set(),2122 schedNoFence::scheduler::mDone: Set(),2123 schedNoFence::scheduler::mExpect: Set(),2124 schedNoFence::scheduler::mResult: Set(),2125 schedNoFence::scheduler::mRetry: Set(),2126 schedNoFence::scheduler::mRevoke: Set(),2127 schedNoFence::scheduler::mSchedule: Set("c1"),2128 schedNoFence::scheduler::published: 1,2129 schedNoFence::scheduler::publishedBy: Set("w1"),2130 schedNoFence::scheduler::ws:2131 Map(2132 "w1" ->2133 {2134 attached: Set(),2135 built: true,2136 expecting: false,2137 running: false,2138 session: false,2139 up: true2140 },2141 "w2" ->2142 {2143 attached: Set(),2144 built: false,2145 expecting: true,2146 running: true,2147 session: true,2148 up: true2149 }2150 )2151}21522153[State 12]2154{2155 schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2156 schedNoFence::scheduler::crashes: 2,2157 schedNoFence::scheduler::entry:2158 [{ followers: Set("c2"), leased: true, worker: "w2" }],2159 schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),2160 schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),2161 schedNoFence::scheduler::mBuild: Set(),2162 schedNoFence::scheduler::mDone: Set("w2"),2163 schedNoFence::scheduler::mExpect: Set(),2164 schedNoFence::scheduler::mResult: Set(),2165 schedNoFence::scheduler::mRetry: Set(),2166 schedNoFence::scheduler::mRevoke: Set(),2167 schedNoFence::scheduler::mSchedule: Set("c1"),2168 schedNoFence::scheduler::published: 2,2169 schedNoFence::scheduler::publishedBy: Set("w1", "w2"),2170 schedNoFence::scheduler::ws:2171 Map(2172 "w1" ->2173 {2174 attached: Set(),2175 built: true,2176 expecting: false,2177 running: false,2178 session: false,2179 up: true2180 },2181 "w2" ->2182 {2183 attached: Set(),2184 built: true,2185 expecting: false,2186 running: false,2187 session: true,2188 up: true2189 }2190 )2191}21922193[violation] Found an issue (3011ms at 7968 traces/second).2194Use --verbosity=3 to show executions.2195Use --seed=0xfb09935243f28a62 --backend=rust to reproduce.2196error: Invariant violated2197An example execution:21982199[State 0]2200{2201 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2202 schedNoPush::scheduler::crashes: 0,2203 schedNoPush::scheduler::entry: [],2204 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2205 schedNoPush::scheduler::mAssigned: Set(),2206 schedNoPush::scheduler::mBuild: Set(),2207 schedNoPush::scheduler::mDone: Set(),2208 schedNoPush::scheduler::mExpect: Set(),2209 schedNoPush::scheduler::mResult: Set(),2210 schedNoPush::scheduler::mRetry: Set(),2211 schedNoPush::scheduler::mRevoke: Set(),2212 schedNoPush::scheduler::mSchedule: Set(),2213 schedNoPush::scheduler::published: 0,2214 schedNoPush::scheduler::publishedBy: Set(),2215 schedNoPush::scheduler::ws:2216 Map(2217 "w1" ->2218 {2219 attached: Set(),2220 built: false,2221 expecting: false,2222 running: false,2223 session: true,2224 up: true2225 },2226 "w2" ->2227 {2228 attached: Set(),2229 built: false,2230 expecting: false,2231 running: false,2232 session: true,2233 up: true2234 }2235 )2236}22372238[State 1]2239{2240 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2241 schedNoPush::scheduler::crashes: 1,2242 schedNoPush::scheduler::entry: [],2243 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2244 schedNoPush::scheduler::mAssigned: Set(),2245 schedNoPush::scheduler::mBuild: Set(),2246 schedNoPush::scheduler::mDone: Set(),2247 schedNoPush::scheduler::mExpect: Set(),2248 schedNoPush::scheduler::mResult: Set(),2249 schedNoPush::scheduler::mRetry: Set(),2250 schedNoPush::scheduler::mRevoke: Set(),2251 schedNoPush::scheduler::mSchedule: Set(),2252 schedNoPush::scheduler::published: 0,2253 schedNoPush::scheduler::publishedBy: Set(),2254 schedNoPush::scheduler::ws:2255 Map(2256 "w1" ->2257 {2258 attached: Set(),2259 built: false,2260 expecting: false,2261 running: false,2262 session: true,2263 up: true2264 },2265 "w2" ->2266 {2267 attached: Set(),2268 built: false,2269 expecting: false,2270 running: false,2271 session: false,2272 up: false2273 }2274 )2275}22762277[State 2]2278{2279 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2280 schedNoPush::scheduler::crashes: 1,2281 schedNoPush::scheduler::entry: [],2282 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2283 schedNoPush::scheduler::mAssigned: Set(),2284 schedNoPush::scheduler::mBuild: Set(),2285 schedNoPush::scheduler::mDone: Set(),2286 schedNoPush::scheduler::mExpect: Set(),2287 schedNoPush::scheduler::mResult: Set(),2288 schedNoPush::scheduler::mRetry: Set(),2289 schedNoPush::scheduler::mRevoke: Set(),2290 schedNoPush::scheduler::mSchedule: Set("c2"),2291 schedNoPush::scheduler::published: 0,2292 schedNoPush::scheduler::publishedBy: Set(),2293 schedNoPush::scheduler::ws:2294 Map(2295 "w1" ->2296 {2297 attached: Set(),2298 built: false,2299 expecting: false,2300 running: false,2301 session: true,2302 up: true2303 },2304 "w2" ->2305 {2306 attached: Set(),2307 built: false,2308 expecting: false,2309 running: false,2310 session: false,2311 up: false2312 }2313 )2314}23152316[State 3]2317{2318 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),2319 schedNoPush::scheduler::crashes: 1,2320 schedNoPush::scheduler::entry:2321 [{ followers: Set("c2"), leased: true, worker: "w1" }],2322 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2323 schedNoPush::scheduler::mAssigned: Set(("c2", "w1")),2324 schedNoPush::scheduler::mBuild: Set(),2325 schedNoPush::scheduler::mDone: Set(),2326 schedNoPush::scheduler::mExpect: Set(),2327 schedNoPush::scheduler::mResult: Set(),2328 schedNoPush::scheduler::mRetry: Set(),2329 schedNoPush::scheduler::mRevoke: Set(),2330 schedNoPush::scheduler::mSchedule: Set(),2331 schedNoPush::scheduler::published: 0,2332 schedNoPush::scheduler::publishedBy: Set(),2333 schedNoPush::scheduler::ws:2334 Map(2335 "w1" ->2336 {2337 attached: Set(),2338 built: false,2339 expecting: false,2340 running: false,2341 session: true,2342 up: true2343 },2344 "w2" ->2345 {2346 attached: Set(),2347 built: false,2348 expecting: false,2349 running: false,2350 session: false,2351 up: false2352 }2353 )2354}23552356[State 4]2357{2358 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2359 schedNoPush::scheduler::crashes: 1,2360 schedNoPush::scheduler::entry:2361 [{ followers: Set("c2"), leased: true, worker: "w1" }],2362 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2363 schedNoPush::scheduler::mAssigned: Set(),2364 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2365 schedNoPush::scheduler::mDone: Set(),2366 schedNoPush::scheduler::mExpect: Set(),2367 schedNoPush::scheduler::mResult: Set(),2368 schedNoPush::scheduler::mRetry: Set(),2369 schedNoPush::scheduler::mRevoke: Set(),2370 schedNoPush::scheduler::mSchedule: Set(),2371 schedNoPush::scheduler::published: 0,2372 schedNoPush::scheduler::publishedBy: Set(),2373 schedNoPush::scheduler::ws:2374 Map(2375 "w1" ->2376 {2377 attached: Set(),2378 built: false,2379 expecting: false,2380 running: false,2381 session: true,2382 up: true2383 },2384 "w2" ->2385 {2386 attached: Set(),2387 built: false,2388 expecting: false,2389 running: false,2390 session: false,2391 up: false2392 }2393 )2394}23952396[State 5]2397{2398 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2399 schedNoPush::scheduler::crashes: 2,2400 schedNoPush::scheduler::entry:2401 [{ followers: Set("c2"), leased: true, worker: "w1" }],2402 schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),2403 schedNoPush::scheduler::mAssigned: Set(),2404 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2405 schedNoPush::scheduler::mDone: Set(),2406 schedNoPush::scheduler::mExpect: Set(),2407 schedNoPush::scheduler::mResult: Set(),2408 schedNoPush::scheduler::mRetry: Set(),2409 schedNoPush::scheduler::mRevoke: Set(),2410 schedNoPush::scheduler::mSchedule: Set(),2411 schedNoPush::scheduler::published: 0,2412 schedNoPush::scheduler::publishedBy: Set(),2413 schedNoPush::scheduler::ws:2414 Map(2415 "w1" ->2416 {2417 attached: Set(),2418 built: false,2419 expecting: false,2420 running: false,2421 session: false,2422 up: false2423 },2424 "w2" ->2425 {2426 attached: Set(),2427 built: false,2428 expecting: false,2429 running: false,2430 session: false,2431 up: false2432 }2433 )2434}24352436[State 6]2437{2438 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2439 schedNoPush::scheduler::crashes: 2,2440 schedNoPush::scheduler::entry: [],2441 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2442 schedNoPush::scheduler::mAssigned: Set(),2443 schedNoPush::scheduler::mBuild: Set(("c2", "w1")),2444 schedNoPush::scheduler::mDone: Set(),2445 schedNoPush::scheduler::mExpect: Set(),2446 schedNoPush::scheduler::mResult: Set(),2447 schedNoPush::scheduler::mRetry: Set("c2"),2448 schedNoPush::scheduler::mRevoke: Set(),2449 schedNoPush::scheduler::mSchedule: Set(),2450 schedNoPush::scheduler::published: 0,2451 schedNoPush::scheduler::publishedBy: Set(),2452 schedNoPush::scheduler::ws:2453 Map(2454 "w1" ->2455 {2456 attached: Set(),2457 built: false,2458 expecting: false,2459 running: false,2460 session: true,2461 up: true2462 },2463 "w2" ->2464 {2465 attached: Set(),2466 built: false,2467 expecting: false,2468 running: false,2469 session: false,2470 up: false2471 }2472 )2473}24742475[State 7]2476{2477 schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CSent("w1")),2478 schedNoPush::scheduler::crashes: 2,2479 schedNoPush::scheduler::entry: [],2480 schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),2481 schedNoPush::scheduler::mAssigned: Set(),2482 schedNoPush::scheduler::mBuild: Set(),2483 schedNoPush::scheduler::mDone: Set(),2484 schedNoPush::scheduler::mExpect: Set(),2485 schedNoPush::scheduler::mResult: Set(),2486 schedNoPush::scheduler::mRetry: Set("c2"),2487 schedNoPush::scheduler::mRevoke: Set(),2488 schedNoPush::scheduler::mSchedule: Set(),2489 schedNoPush::scheduler::published: 0,2490 schedNoPush::scheduler::publishedBy: Set(),2491 schedNoPush::scheduler::ws:2492 Map(2493 "w1" ->2494 {2495 attached: Set("c2"),2496 built: false,2497 expecting: true,2498 running: true,2499 session: true,2500 up: true2501 },2502 "w2" ->2503 {2504 attached: Set(),2505 built: false,2506 expecting: false,2507 running: false,2508 session: false,2509 up: false2510 }2511 )2512}25132514[violation] Found an issue (1312ms at 9738 traces/second).2515Use --verbosity=3 to show executions.2516Use --seed=0xcc1a36287dedc910 --backend=rust to reproduce.2517error: Invariant violated2518An example execution:25192520[State 0]2521{2522 schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),2523 schedNoReport::scheduler::crashes: 0,2524 schedNoReport::scheduler::entry: [],2525 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2526 schedNoReport::scheduler::mAssigned: Set(),2527 schedNoReport::scheduler::mBuild: Set(),2528 schedNoReport::scheduler::mDone: Set(),2529 schedNoReport::scheduler::mExpect: Set(),2530 schedNoReport::scheduler::mResult: Set(),2531 schedNoReport::scheduler::mRetry: Set(),2532 schedNoReport::scheduler::mRevoke: Set(),2533 schedNoReport::scheduler::mSchedule: Set(),2534 schedNoReport::scheduler::published: 0,2535 schedNoReport::scheduler::publishedBy: Set(),2536 schedNoReport::scheduler::ws:2537 Map(2538 "w1" ->2539 {2540 attached: Set(),2541 built: false,2542 expecting: false,2543 running: false,2544 session: true,2545 up: true2546 },2547 "w2" ->2548 {2549 attached: Set(),2550 built: false,2551 expecting: false,2552 running: false,2553 session: true,2554 up: true2555 }2556 )2557}25582559[State 1]2560{2561 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2562 schedNoReport::scheduler::crashes: 0,2563 schedNoReport::scheduler::entry: [],2564 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2565 schedNoReport::scheduler::mAssigned: Set(),2566 schedNoReport::scheduler::mBuild: Set(),2567 schedNoReport::scheduler::mDone: Set(),2568 schedNoReport::scheduler::mExpect: Set(),2569 schedNoReport::scheduler::mResult: Set(),2570 schedNoReport::scheduler::mRetry: Set(),2571 schedNoReport::scheduler::mRevoke: Set(),2572 schedNoReport::scheduler::mSchedule: Set("c1"),2573 schedNoReport::scheduler::published: 0,2574 schedNoReport::scheduler::publishedBy: Set(),2575 schedNoReport::scheduler::ws:2576 Map(2577 "w1" ->2578 {2579 attached: Set(),2580 built: false,2581 expecting: false,2582 running: false,2583 session: true,2584 up: true2585 },2586 "w2" ->2587 {2588 attached: Set(),2589 built: false,2590 expecting: false,2591 running: false,2592 session: true,2593 up: true2594 }2595 )2596}25972598[State 2]2599{2600 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2601 schedNoReport::scheduler::crashes: 0,2602 schedNoReport::scheduler::entry:2603 [{ followers: Set("c1"), leased: true, worker: "w2" }],2604 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2605 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2606 schedNoReport::scheduler::mBuild: Set(),2607 schedNoReport::scheduler::mDone: Set(),2608 schedNoReport::scheduler::mExpect: Set("w2"),2609 schedNoReport::scheduler::mResult: Set(),2610 schedNoReport::scheduler::mRetry: Set(),2611 schedNoReport::scheduler::mRevoke: Set(),2612 schedNoReport::scheduler::mSchedule: Set(),2613 schedNoReport::scheduler::published: 0,2614 schedNoReport::scheduler::publishedBy: Set(),2615 schedNoReport::scheduler::ws:2616 Map(2617 "w1" ->2618 {2619 attached: Set(),2620 built: false,2621 expecting: false,2622 running: false,2623 session: true,2624 up: true2625 },2626 "w2" ->2627 {2628 attached: Set(),2629 built: false,2630 expecting: false,2631 running: false,2632 session: true,2633 up: true2634 }2635 )2636}26372638[State 3]2639{2640 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2641 schedNoReport::scheduler::crashes: 1,2642 schedNoReport::scheduler::entry:2643 [{ followers: Set("c1"), leased: true, worker: "w2" }],2644 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2645 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2646 schedNoReport::scheduler::mBuild: Set(),2647 schedNoReport::scheduler::mDone: Set(),2648 schedNoReport::scheduler::mExpect: Set("w2"),2649 schedNoReport::scheduler::mResult: Set(),2650 schedNoReport::scheduler::mRetry: Set(),2651 schedNoReport::scheduler::mRevoke: Set(),2652 schedNoReport::scheduler::mSchedule: Set(),2653 schedNoReport::scheduler::published: 0,2654 schedNoReport::scheduler::publishedBy: Set(),2655 schedNoReport::scheduler::ws:2656 Map(2657 "w1" ->2658 {2659 attached: Set(),2660 built: false,2661 expecting: false,2662 running: false,2663 session: false,2664 up: false2665 },2666 "w2" ->2667 {2668 attached: Set(),2669 built: false,2670 expecting: false,2671 running: false,2672 session: true,2673 up: true2674 }2675 )2676}26772678[State 4]2679{2680 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2681 schedNoReport::scheduler::crashes: 1,2682 schedNoReport::scheduler::entry:2683 [{ followers: Set("c1"), leased: true, worker: "w2" }],2684 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),2685 schedNoReport::scheduler::mAssigned: Set(("c1", "w2")),2686 schedNoReport::scheduler::mBuild: Set(),2687 schedNoReport::scheduler::mDone: Set(),2688 schedNoReport::scheduler::mExpect: Set(),2689 schedNoReport::scheduler::mResult: Set(),2690 schedNoReport::scheduler::mRetry: Set(),2691 schedNoReport::scheduler::mRevoke: Set(),2692 schedNoReport::scheduler::mSchedule: Set(),2693 schedNoReport::scheduler::published: 0,2694 schedNoReport::scheduler::publishedBy: Set(),2695 schedNoReport::scheduler::ws:2696 Map(2697 "w1" ->2698 {2699 attached: Set(),2700 built: false,2701 expecting: false,2702 running: false,2703 session: false,2704 up: false2705 },2706 "w2" ->2707 {2708 attached: Set(),2709 built: false,2710 expecting: true,2711 running: true,2712 session: true,2713 up: true2714 }2715 )2716}27172718[State 5]2719{2720 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),2721 schedNoReport::scheduler::crashes: 2,2722 schedNoReport::scheduler::entry: [],2723 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2724 schedNoReport::scheduler::mAssigned: Set(),2725 schedNoReport::scheduler::mBuild: Set(),2726 schedNoReport::scheduler::mDone: Set(),2727 schedNoReport::scheduler::mExpect: Set(),2728 schedNoReport::scheduler::mResult: Set(),2729 schedNoReport::scheduler::mRetry: Set("c1"),2730 schedNoReport::scheduler::mRevoke: Set(),2731 schedNoReport::scheduler::mSchedule: Set(),2732 schedNoReport::scheduler::published: 0,2733 schedNoReport::scheduler::publishedBy: Set(),2734 schedNoReport::scheduler::ws:2735 Map(2736 "w1" ->2737 {2738 attached: Set(),2739 built: false,2740 expecting: false,2741 running: false,2742 session: false,2743 up: false2744 },2745 "w2" ->2746 {2747 attached: Set(),2748 built: false,2749 expecting: true,2750 running: true,2751 session: false,2752 up: true2753 }2754 )2755}27562757[State 6]2758{2759 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2760 schedNoReport::scheduler::crashes: 2,2761 schedNoReport::scheduler::entry: [],2762 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2763 schedNoReport::scheduler::mAssigned: Set(),2764 schedNoReport::scheduler::mBuild: Set(),2765 schedNoReport::scheduler::mDone: Set(),2766 schedNoReport::scheduler::mExpect: Set(),2767 schedNoReport::scheduler::mResult: Set(),2768 schedNoReport::scheduler::mRetry: Set("c1"),2769 schedNoReport::scheduler::mRevoke: Set(),2770 schedNoReport::scheduler::mSchedule: Set("c2"),2771 schedNoReport::scheduler::published: 0,2772 schedNoReport::scheduler::publishedBy: Set(),2773 schedNoReport::scheduler::ws:2774 Map(2775 "w1" ->2776 {2777 attached: Set(),2778 built: false,2779 expecting: false,2780 running: false,2781 session: false,2782 up: false2783 },2784 "w2" ->2785 {2786 attached: Set(),2787 built: false,2788 expecting: true,2789 running: true,2790 session: false,2791 up: true2792 }2793 )2794}27952796[State 7]2797{2798 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2799 schedNoReport::scheduler::crashes: 2,2800 schedNoReport::scheduler::entry: [],2801 schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),2802 schedNoReport::scheduler::mAssigned: Set(),2803 schedNoReport::scheduler::mBuild: Set(),2804 schedNoReport::scheduler::mDone: Set(),2805 schedNoReport::scheduler::mExpect: Set(),2806 schedNoReport::scheduler::mResult: Set(),2807 schedNoReport::scheduler::mRetry: Set("c1"),2808 schedNoReport::scheduler::mRevoke: Set(),2809 schedNoReport::scheduler::mSchedule: Set("c2"),2810 schedNoReport::scheduler::published: 0,2811 schedNoReport::scheduler::publishedBy: Set(),2812 schedNoReport::scheduler::ws:2813 Map(2814 "w1" ->2815 {2816 attached: Set(),2817 built: false,2818 expecting: false,2819 running: false,2820 session: true,2821 up: true2822 },2823 "w2" ->2824 {2825 attached: Set(),2826 built: false,2827 expecting: true,2828 running: true,2829 session: false,2830 up: true2831 }2832 )2833}28342835[State 8]2836{2837 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2838 schedNoReport::scheduler::crashes: 2,2839 schedNoReport::scheduler::entry:2840 [{ followers: Set("c2"), leased: true, worker: "w1" }],2841 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2842 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2843 schedNoReport::scheduler::mBuild: Set(),2844 schedNoReport::scheduler::mDone: Set(),2845 schedNoReport::scheduler::mExpect: Set("w1"),2846 schedNoReport::scheduler::mResult: Set(),2847 schedNoReport::scheduler::mRetry: Set("c1"),2848 schedNoReport::scheduler::mRevoke: Set(),2849 schedNoReport::scheduler::mSchedule: Set(),2850 schedNoReport::scheduler::published: 0,2851 schedNoReport::scheduler::publishedBy: Set(),2852 schedNoReport::scheduler::ws:2853 Map(2854 "w1" ->2855 {2856 attached: Set(),2857 built: false,2858 expecting: false,2859 running: false,2860 session: true,2861 up: true2862 },2863 "w2" ->2864 {2865 attached: Set(),2866 built: false,2867 expecting: true,2868 running: true,2869 session: false,2870 up: true2871 }2872 )2873}28742875[State 9]2876{2877 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),2878 schedNoReport::scheduler::crashes: 2,2879 schedNoReport::scheduler::entry:2880 [{ followers: Set("c2"), leased: true, worker: "w1" }],2881 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2882 schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),2883 schedNoReport::scheduler::mBuild: Set(),2884 schedNoReport::scheduler::mDone: Set(),2885 schedNoReport::scheduler::mExpect: Set("w1"),2886 schedNoReport::scheduler::mResult: Set(),2887 schedNoReport::scheduler::mRetry: Set("c1"),2888 schedNoReport::scheduler::mRevoke: Set(),2889 schedNoReport::scheduler::mSchedule: Set(),2890 schedNoReport::scheduler::published: 0,2891 schedNoReport::scheduler::publishedBy: Set(),2892 schedNoReport::scheduler::ws:2893 Map(2894 "w1" ->2895 {2896 attached: Set(),2897 built: false,2898 expecting: false,2899 running: false,2900 session: true,2901 up: true2902 },2903 "w2" ->2904 {2905 attached: Set(),2906 built: false,2907 expecting: true,2908 running: true,2909 session: true,2910 up: true2911 }2912 )2913}29142915[State 10]2916{2917 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2918 schedNoReport::scheduler::crashes: 2,2919 schedNoReport::scheduler::entry:2920 [{ followers: Set("c2"), leased: true, worker: "w1" }],2921 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2922 schedNoReport::scheduler::mAssigned: Set(),2923 schedNoReport::scheduler::mBuild: Set(("c2", "w1")),2924 schedNoReport::scheduler::mDone: Set(),2925 schedNoReport::scheduler::mExpect: Set("w1"),2926 schedNoReport::scheduler::mResult: Set(),2927 schedNoReport::scheduler::mRetry: Set("c1"),2928 schedNoReport::scheduler::mRevoke: Set(),2929 schedNoReport::scheduler::mSchedule: Set(),2930 schedNoReport::scheduler::published: 0,2931 schedNoReport::scheduler::publishedBy: Set(),2932 schedNoReport::scheduler::ws:2933 Map(2934 "w1" ->2935 {2936 attached: Set(),2937 built: false,2938 expecting: false,2939 running: false,2940 session: true,2941 up: true2942 },2943 "w2" ->2944 {2945 attached: Set(),2946 built: false,2947 expecting: true,2948 running: true,2949 session: true,2950 up: true2951 }2952 )2953}29542955[State 11]2956{2957 schedNoReport::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),2958 schedNoReport::scheduler::crashes: 2,2959 schedNoReport::scheduler::entry:2960 [{ followers: Set("c2"), leased: true, worker: "w1" }],2961 schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),2962 schedNoReport::scheduler::mAssigned: Set(),2963 schedNoReport::scheduler::mBuild: Set(("c2", "w1")),2964 schedNoReport::scheduler::mDone: Set(),2965 schedNoReport::scheduler::mExpect: Set(),2966 schedNoReport::scheduler::mResult: Set(),2967 schedNoReport::scheduler::mRetry: Set("c1"),2968 schedNoReport::scheduler::mRevoke: Set(),2969 schedNoReport::scheduler::mSchedule: Set(),2970 schedNoReport::scheduler::published: 0,2971 schedNoReport::scheduler::publishedBy: Set(),2972 schedNoReport::scheduler::ws:2973 Map(2974 "w1" ->2975 {2976 attached: Set(),2977 built: false,2978 expecting: true,2979 running: true,2980 session: true,2981 up: true2982 },2983 "w2" ->2984 {2985 attached: Set(),2986 built: false,2987 expecting: true,2988 running: true,2989 session: true,2990 up: true2991 }2992 )2993}29942995[violation] Found an issue (1734ms at 13326 traces/second).2996Use --verbosity=3 to show executions.2997Use --seed=0x65d9f5baa938815b --backend=rust to reproduce.2998error: Invariant violated2999An example execution:30003001[State 0]3002{3003 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3004 schedTerminal::scheduler::crashes: 0,3005 schedTerminal::scheduler::entry: [],3006 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3007 schedTerminal::scheduler::mAssigned: Set(),3008 schedTerminal::scheduler::mBuild: Set(),3009 schedTerminal::scheduler::mDone: Set(),3010 schedTerminal::scheduler::mExpect: Set(),3011 schedTerminal::scheduler::mResult: Set(),3012 schedTerminal::scheduler::mRetry: Set(),3013 schedTerminal::scheduler::mRevoke: Set(),3014 schedTerminal::scheduler::mSchedule: Set(),3015 schedTerminal::scheduler::published: 0,3016 schedTerminal::scheduler::publishedBy: Set(),3017 schedTerminal::scheduler::ws:3018 Map(3019 "w1" ->3020 {3021 attached: Set(),3022 built: false,3023 expecting: false,3024 running: false,3025 session: true,3026 up: true3027 },3028 "w2" ->3029 {3030 attached: Set(),3031 built: false,3032 expecting: false,3033 running: false,3034 session: true,3035 up: true3036 }3037 )3038}30393040[State 1]3041{3042 schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),3043 schedTerminal::scheduler::crashes: 1,3044 schedTerminal::scheduler::entry: [],3045 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3046 schedTerminal::scheduler::mAssigned: Set(),3047 schedTerminal::scheduler::mBuild: Set(),3048 schedTerminal::scheduler::mDone: Set(),3049 schedTerminal::scheduler::mExpect: Set(),3050 schedTerminal::scheduler::mResult: Set(),3051 schedTerminal::scheduler::mRetry: Set(),3052 schedTerminal::scheduler::mRevoke: Set(),3053 schedTerminal::scheduler::mSchedule: Set(),3054 schedTerminal::scheduler::published: 0,3055 schedTerminal::scheduler::publishedBy: Set(),3056 schedTerminal::scheduler::ws:3057 Map(3058 "w1" ->3059 {3060 attached: Set(),3061 built: false,3062 expecting: false,3063 running: false,3064 session: false,3065 up: true3066 },3067 "w2" ->3068 {3069 attached: Set(),3070 built: false,3071 expecting: false,3072 running: false,3073 session: false,3074 up: true3075 }3076 )3077}30783079[State 2]3080{3081 schedTerminal::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),3082 schedTerminal::scheduler::crashes: 1,3083 schedTerminal::scheduler::entry: [],3084 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3085 schedTerminal::scheduler::mAssigned: Set(),3086 schedTerminal::scheduler::mBuild: Set(),3087 schedTerminal::scheduler::mDone: Set(),3088 schedTerminal::scheduler::mExpect: Set(),3089 schedTerminal::scheduler::mResult: Set(),3090 schedTerminal::scheduler::mRetry: Set(),3091 schedTerminal::scheduler::mRevoke: Set(),3092 schedTerminal::scheduler::mSchedule: Set("c1"),3093 schedTerminal::scheduler::published: 0,3094 schedTerminal::scheduler::publishedBy: Set(),3095 schedTerminal::scheduler::ws:3096 Map(3097 "w1" ->3098 {3099 attached: Set(),3100 built: false,3101 expecting: false,3102 running: false,3103 session: false,3104 up: true3105 },3106 "w2" ->3107 {3108 attached: Set(),3109 built: false,3110 expecting: false,3111 running: false,3112 session: false,3113 up: true3114 }3115 )3116}31173118[State 3]3119{3120 schedTerminal::scheduler::cl: Map("c1" -> CFailed, "c2" -> CIdle),3121 schedTerminal::scheduler::crashes: 1,3122 schedTerminal::scheduler::entry: [],3123 schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1),3124 schedTerminal::scheduler::mAssigned: Set(),3125 schedTerminal::scheduler::mBuild: Set(),3126 schedTerminal::scheduler::mDone: Set(),3127 schedTerminal::scheduler::mExpect: Set(),3128 schedTerminal::scheduler::mResult: Set(),3129 schedTerminal::scheduler::mRetry: Set(),3130 schedTerminal::scheduler::mRevoke: Set(),3131 schedTerminal::scheduler::mSchedule: Set(),3132 schedTerminal::scheduler::published: 0,3133 schedTerminal::scheduler::publishedBy: Set(),3134 schedTerminal::scheduler::ws:3135 Map(3136 "w1" ->3137 {3138 attached: Set(),3139 built: false,3140 expecting: false,3141 running: false,3142 session: false,3143 up: true3144 },3145 "w2" ->3146 {3147 attached: Set(),3148 built: false,3149 expecting: false,3150 running: false,3151 session: false,3152 up: true3153 }3154 )3155}31563157[violation] Found an issue (694ms at 1424 traces/second).3158Use --verbosity=3 to show executions.3159Use --seed=0xe76c235268460128 --backend=rust to reproduce.3160error: Invariant violated3161An example execution:31623163[State 0]3164{3165 pushFixed::push::byPath: Map(),3166 pushFixed::push::inflight: Set(),3167 pushFixed::push::left: Map(),3168 pushFixed::push::sent: Map()3169}31703171[State 1]3172{3173 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3174 pushFixed::push::inflight: Set((1, "a"), (1, "b")),3175 pushFixed::push::left: Map(1 -> 2),3176 pushFixed::push::sent: Map(1 -> Set("a", "b"))3177}31783179[State 2]3180{3181 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3182 pushFixed::push::inflight: Set((1, "b")),3183 pushFixed::push::left: Map(1 -> 1),3184 pushFixed::push::sent: Map(1 -> Set("a", "b"))3185}31863187[State 3]3188{3189 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),3190 pushFixed::push::inflight: Set(),3191 pushFixed::push::left: Map(1 -> 0),3192 pushFixed::push::sent: Map(1 -> Set("a", "b"))3193}31943195[State 4]3196{3197 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),3198 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3199 pushFixed::push::left: Map(1 -> 0, 3 -> 2),3200 pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b"))3201}32023203[State 5]3204{3205 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3206 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a"), (3, "b")),3207 pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 2),3208 pushFixed::push::sent:3209 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3210}32113212[State 6]3213{3214 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3215 pushFixed::push::inflight: Set((2, "a"), (3, "a"), (3, "b")),3216 pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 2),3217 pushFixed::push::sent:3218 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3219}32203221[State 7]3222{3223 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3224 pushFixed::push::inflight: Set((3, "a"), (3, "b")),3225 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 2),3226 pushFixed::push::sent:3227 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3228}32293230[State 8]3231{3232 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3233 pushFixed::push::inflight: Set((3, "b")),3234 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1),3235 pushFixed::push::sent:3236 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3237}32383239[State 9]3240{3241 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),3242 pushFixed::push::inflight: Set(),3243 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),3244 pushFixed::push::sent:3245 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))3246}32473248[ok] No violation found (558ms at 35842 traces/second).3249Trace length statistics: max=10, min=7, average=8.123250You may increase --max-samples and --max-steps.3251Use --verbosity to produce more (or less) output.3252Use --seed=0x1c6adf4e784019dd --backend=rust to reproduce.